数学家Hales撰文讨论Lean形式化数学的可靠性。2026年AI自动形式化取得突破，Fermat大定理等被快速形式化，但同年夏季发现多个Lean内核可靠性漏洞，可证明假命题。应对方案包括多内核交叉验证、形式化验证内核（如Con-Leche）及加强类型论元理论研究。作者警告AI时代不可盲信系统，需人类审计。

陶哲轩博客发布Annalisa Buffa的客座文章，宣布EPFL数值建模与仿真教席招聘博士后，探索形式化验证与算法发现对数值分析的影响。研究方向包括用Lean形式化有限元稳定性与误差估计，或AI辅助发现新离散范式并形式验证。无固定项目，需主导新研究线并发表成果。申请需提交CV、动机信和两名推荐人，招满为止。

陶哲轩等人宣布启动Lean内核挑战赛第一阶段，旨在提升Lean 4内核验证计算的性能。比赛设八个问题：斐波那契、整数分拆、梅尔滕斯函数、素数计数、矩阵积和式、Rule 110、SHA-256和多项式判别式。参赛者需用Lean开发算法并证明其符合规范。截止日期为2026年11月20日，由Lean FRO与SAIR基金会合办。

本期周刊聚焦 Laravel 禁止提交 issue、只收 PR，认为可减少垃圾反馈、方便维护者，AI 时代提交 PR 已不困难。Anthropic 用 Claude 历时11天将怀尔斯费马大定理证明译为 Lean 语言，生成1300万行代码，为史上最长数学程序。此外还介绍特斯拉 Cybercab、戴森电动牙刷、AI 手杖等科技动态，以及多篇文章、工具、资源和言论。

Anthropic宣布Claude用11天完成费马大定理的端到端形式化证明，生成约1300万行Lean代码和超3万个中间定理，规模超Mathlib五倍。通过Prove2Me平台协调多Agent协作，消耗60亿Token，人类指导有限。这标志AI可大规模自动化数学形式化，同时OpenAI正推广GPT-6 Astra。

Lean语言创始人Leo de Moura讨论如何用Lean证明AI代理的正确性，结合自动推理与概率模型，并利用AI持续优化代码。Lean作为函数式编程语言和证明助手，可在同一系统中验证程序数学正确性。

陶哲轩宣布Palomar数学验证注册表开放提交，旨在验证Lean证明的可靠性。该注册表由Lean FRO和ICARM孵化，检查代码是否通过类型检查、无额外公理，且形式化陈述与描述匹配。提交需通过机械检查和AI模型验证，但非同行评审。陶哲轩已成功提交Sendov猜想证明，欢迎新旧结果及AI辅助提交。

2026年，形式验证因AI辅助而复兴，Lean语言成为热门。文章回顾1979年论文的批评，指出验证虽进步，但规格说明翻译、全自动验证、验证后防御等挑战犹存。AI提升证明效率，但验证者正确性、社会过程等根本问题未解，验证仅是可靠性拼图之一。

斯坦福大学的Lean LaunchPad课程已举办16年，旨在帮助创业者寻找可重复和可扩展的商业模式。课程强调实践与结构，学生需进行客户访谈并开发最小可行产品（MVP）。今年首次引入AI工具，提升了客户发现的效率，但也导致学生对产品与市场契合的理解出现偏差。未来将要求学生在带入原型的同时，明确假设和验证实验。

斯坦福大学的Lean LaunchPad课程已举办15届，旨在帮助创业者寻找可重复和可扩展的商业模式。课程强调实践与结构，要求学生每周进行客户访谈并开发最小可行产品。该课程已在多所大学推广，培养了大量科学家和工程师，并获得显著风险投资。AI工具的应用也在课程中逐渐增多，推动了创业教育的变革。

作者计划为20年前的实分析教材《Analysis I》推出Lean伴侣，将书中的定义、定理和习题转化为Lean代码，以便于使用证明助手进行验证。该伴侣将逐步依赖Mathlib库，帮助学生在学习实分析的同时掌握Lean编程。