一大早被震撼到了！
Claude刚刚搞定了一件数学界原本以为要啃很多年的硬骨头。
它在11天内，近乎全自主地写出了费马大定理的完整机器验证代码。
这是有史以来规模最大的一套Lean形式化证明。
总代码量超过1300万行，相当于整个数学公共库Mathlib规模的5倍以上。
为了拿下费马大定理，Claude在途中顺手推导并证明了29500个衍生定理，覆盖了代数、调和分析、几何和数论等多个此前从未被形式化过的数学领域。
官方博客与完整代码均已公开：
博客链接：
https://anthropic.com/research/formalizing-fermats-last-theorem
GitHub开源地址：
https://github.com/anthropics/fermats-last-theorem
困扰人类350年的空白
1637年左右，法国数学家皮埃尔·德·费马在阅读丢番图的算术一书时，在页面边缘写下一个断言：当n大于2时，不存在正整数a、b、c满足a的n次方加b的n次方等于c的n次方。
他当时还留下一句著名的话：我发现了一个真正奇妙的证明，可惜这里的空白太小，写不下。
为了填补这段空白，人类数学家找了350多年。
1908年，德国设立了10万马克巨奖悬赏正确证明，折合现在一两百万美元，仅第一年就收到了621个错误解答。
直到1995年，安德鲁·怀尔斯才彻底攻克了这个难题。
怀尔斯在1993年6月做了三天系列演讲，拿出了长达129页的证明草稿。
但在同行密集审查两个月后，审稿人提出了一个直击要害的问题，证明过程存在致命漏洞。
怀尔斯闭关苦思了一年，先是独自尝试，后来与学生理查德·泰勒合作，在濒临放弃的关头终于找到修复方法，并于1995年5月正式发表了论文。
现代数学界普遍认为，当年费马自己脑海里的奇妙证明大概率是错的，因为怀尔斯的证明用到了17世纪根本不存在的现代数学工具。
这套证明凝结了无数数学家的智慧，融合了弗雷、塞尔、里贝特、梅祖尔、朗兰兹、塔内尔、谷山丰、志村五郎以及韦伊等人的开创性工作。
为什么要让机器来做终审
数学论文是写给人看的，往往会默认跳过许多显而易见的步骤，并且默认建立在几个世纪以来的海量文献之上。
但对计算机来说，它不懂什么是显然成立。
像Lean这样的交互式定理证明工具，要求把一切推理拆解为机器能读懂的逻辑形式，从最基础的数学公理开始，一步一步推演。
如果一环出错，后面的整条逻辑链都会失效。
只要Lean最终编译通过，就代表这个证明在逻辑上百分之百成立，没有任何纰漏。
2005年，荷兰计算机科学家Jan Bergstra首次提议对怀尔斯的证明进行形式化。
2024年，帝国理工学院的数学家凯文·巴扎德在社区发起了这项浩大的工程，光是描述初始阶段规划的蓝图就写了86页，大家原本预计这需要全球数学家合力耗费数年。
Anthropic研究员Tianyi Peng决定测试AI能否加速这一进程。
主持这项研究的Tianyi Peng背景很硬核。
他早年是信息学竞赛顶尖选手，曾拿下全国青少年信息学奥赛选拔赛第八名，2017年本科毕业于清华姚班，随后在2023年拿到麻省理工学院（MIT）博士学位。
目前他担任哥伦比亚大学助理教授，同时也是Anthropic的研究员，长期在哥大带领团队主攻强化学习、AI智能体以及形式化工具研发。
Tianyi Peng本科时就吃过没有形式化验证的亏。
当年导师想把他论文里的成果推荐发表到Nature，问他能不能确保证明完全没有差错。Tianyi Peng老实回答说只有99%的确信度，这么长的证明很难做到100%肯定，最终这项成果错失了登上顶刊的机会。
人类审查极长极复杂的数学证明极其吃力。
1998年托马斯·海尔斯证明开普勒猜想，12位审稿人花了4年时间审核，最后只能得出99%可能正确的结论，海尔斯后来不得不组织二十多人的团队通过Flyspeck项目耗时多年做形式化验证。
佩雷尔曼搞定庞加莱猜想，数学界花了4年写了3部数百页的详尽解析才敢确认。
哈拉尔德·赫尔夫戈特在2013年给出的弱哥德巴赫猜想证明，至今依然处于同行评审状态中。
数学界有时甚至会接受错误的成果长达数年，导致后续学者在有缺陷的基础上搭建理论。
机器形式化验证，正是解决这个信任危机的终极手段。
11天与60亿Token的攻坚
Tianyi Peng团队给Claude设定的证明路线，参考了达蒙、戴蒙德和泰勒对怀尔斯证明的精简阐述版本。
所使用的模型是一个能力大致相当于Claude Fable 5.1的通用内部研究模型。
【费马大定理形式化推进的时间演变过程（Time progression of FLT formalization）】
最初的尝试并不顺利。
智能体虽然早期取得了一些进展，但很快会丢失整个项目的全局状态，无法有效协同，最终代码里有大约7%的行数属于这种失败的无效劳动。
转机发生在团队引入了哥伦比亚大学研发的Prove2Me协同平台。
【Claude用于形式化费马大定理的Prove2Me规划关键里程碑图。三个彩色部分对应Claude在实现最终目标过程中必须证明的三个核心子定理，该图紧密遵循怀尔斯的原始证明路径。】
Prove2Me主要做了三件事：
第一，建立定理的有向无环图，智能体能清晰看到整体进展和依赖树，决定下一步该攻克哪一个子定理，解决了上下文遗忘问题，支持多个智能体并行工作。
第二，把定理的陈述与具体证明过程分拆到不同文件中，独立维护它们之间的链接，大幅降低了计算资源消耗，提升了Lean的编译效率。
第三，为每个定理维护自然语言层面的描述，方便智能体在庞大的知识库中快速检索和复用结论，找到了更简短的证明路径。
几十个Claude智能体开始分工协作，定义概念、证明中间定理，并用这些定理去攻克更难的命题。
人类在其中的干预极少，仅仅是Tianyi Peng偶尔给出几句宏观方向提示，比如提示把雅可比作为方案的优先级调高，或者催促尽快推进梅祖尔定理。
Claude完整思考日志PDF：
https://www-cdn.anthropic.com/9e431dff043da6538d99d6c2d231b670aa3da263.pdf
在证明闭环的那一刻，Claude内部的监控日志记录下了它的状态：
Prove2Me站点上的费马大定理根节点显示已证明，属于历史性时刻。
R等于T闭合并级联到根节点，这是本次任务的核心目标。
在协调世界时8月18日凌晨2点，费马大定理根节点状态被标记为已解决。
最终，Claude一共尝试证明了30300个定理，其中29500个被采纳进最终证明，消耗了大约60亿输出Token。
整个证明只依赖Lean的三条标准公理，并且经过了比对工具确认，其最终陈述与Mathlib库中对费马大定理的定义完全一致。
这对未来的数学研究意味着什么
与近期AI在黎曼猜想中尝试提出全新数学思路不同，这次工作的突破点在于全流程的自动验证。
在查看了这份Lean代码后，凯文·巴扎德评价：
这项非凡的自动形式化成果仅用了11天，除了数学公理外没有任何额外假设。我们看到代数、调和分析、几何和数论被自动化形式化，这证明AI生成的中间产物已经足够稳固，可以层层向上构建。如果费马大定理的自动形式化在今天已经可行，那么现代数学文献的全面机器验证就迈出了一大步。
AI写Lean代码不仅能做核验，还能反哺新数学成果的发现。
研究人员注意到，Claude在很多新探索中会一边推导一边写形式化证明，就像用数值模拟来检验思路一样，借助这些部分证明来独立核验自己的猜想是否走在正确轨道上。
形式化大定理并不是算力巨头的专属特权。
研究团队用3个普通的Claude Max个人订阅账号做了一次实验，同样依托Prove2Me平台，让智能体协作使用哈代李特尔伍德圆法，仅用3天就完成了维诺格拉多夫三素数定理的形式化验证。
这意味着，普通研究人员使用消费级订阅完成重大数学命题的形式化，已经具备了实操可行性。
为了推动这一趋势，Anthropic正在联合其他实验室扩大对外部数学家的支持，包括提供免费和折扣的订阅、科研算力额度，以及为形式化其他重大定理、改进Lean与Mathlib的科研项目提供专门资助。
人类数学家此前耗费数年甚至数十年做审查的沉重负担，正在被机器彻底卸下。
参考资料
Tianyi Peng团队关于协作平台的最新论文：Prove2Me: An open collaborative platform for scaling math formalization，arXiv链接：
https://doi.org/10.48550/arXiv.2608.28433
GitHub仓库中包含完整的代码实现以及证明步骤的详细文字解读。
--end--
最后记得⭐️我，每天都在更新：如果觉得文章还不错的话可以点赞转发推荐评论
/...@作者：你说的完全正确（YAR师）
热门跟贴