人类和费马大定理纠缠了三个半世纪，Claude 这次只用了 11 天！？
刚刚，Anthropic 宣布，Claude 完成了首个端到端、可由计算机完整检查的费马大定理证明。
约 1300 万行 Lean 代码、超过 3 万个中间定理、最终证明使用其中约 29500 个。
整个工程规模，已经超过 Lean 核心数学库 Mathlib 的 5 倍。
它完成的是另一件同样工程量《惊人》的工作：
把人类数学家能够读懂的证明，彻底翻译成计算机能够一行一行检查、没有任何「这里显然」的形式化证明。
而这件事，数学界原本是按多年工程来准备的？？？？
先快速说一下费马大定理到底是什么。
其指的是，对于任意整数 n>2，都不存在正整数 a、b、c，使：a +b =c 。
这个命题看起来极其简单，难度却高得离谱！！
从 17 世纪费马留下这个命题开始，欧拉、勒让德、库默尔等一代代数学家不断往前推进，始终没能拿下完整证明。
直到 1993 年，英国数学家 Andrew Wiles 第一次公开宣布证明费马大定理。
随后审查发现其中存在关键缺口。
Wiles 又花了大约一年时间和 Richard Taylor 一起修补，最终在 1994 年完成证明，到这里，困扰数学界 350 多年的命题才终于被攻克。。。
能不能让计算机，也百分之百确认这份证明成立捏？
这就是所谓的「形式化」。
简单理解，普通数学论文是写给数学家看的，人脑看到很多步骤，可以直接说：嗯，这里显然成立～
但 Lean 这种专门检查数学证明的程序系统证明助手，可不吃这一套。。。
我们可以把 Lean 理解成数学世界里的「超级严格编译器」——
数学家或者 AI 负责把定理、定义和证明一步一步写成 Lean 能够理解的形式；Lean 则负责检查，每一个推导到底有没有从前面的公理和定理合法地走出来。
这也是为什么形式化一个大型现代数学证明，工作量经常大得惊人！！
2000 年代，计算机科学家就已经提出过形式化 Wiles 证明的设想。
到 2024 年，帝国理工学院 Kevin Buzzard 等人才正式启动一个多年社区项目，准备使用 Lean 完成费马大定理形式化，光项目第一阶段的技术蓝图，就写了 86 页。
结果 Claude 来了之后：11 天。
作为早年是信息学竞赛尖子，Tianyi Peng 曾获全国青少年信息学奥赛选拔赛第八名，2017 年从清华姚班本科毕业，2023 年获 MIT 博士学位。
如今，他是哥伦比亚大学助理教授、Anthropic 研究员，长期聚焦强化学习、AI Agent 与形式化工具。
开始吧，他只是想测试一下，Claude 究竟能把这个项目往前推多远。
最后，没成想，Claude 直接一路干到了终点。。。
有的负责补数学定义，有的专门攻中间引理，有的沿着已有成果继续往更高层定理推进，还有 Agent 负责把不同部分重新拼回整个证明体系。
最后堆出来的成果，是约 1300 万行 Lean 代码、超过 3 万个中间定理。
而这个代码量，甚至超过 Lean 核心数学库 Mathlib 自身规模的 5 倍！！！
Anthropic 对此也表示，完整证明只依赖 Lean 三个标准公理，而且他们还专门通过比较程序确认，Claude 最终证明的定理陈述，与 Mathlib 里的费马大定理完全一致。
也就是说，至少在逻辑检查这件事上，不能靠模型自己说「我证明完了」。
而裁判，正是 Lean。
Claude 也曾组团组到失忆，最后靠 Harness 救回来
不过 Claude 这 11 天，也没一路开挂到底。
项目刚开始时，多 Agent 协作很快撞上了一个如今几乎所有大型 Agent 系统都会遇到的问题——
人一多，活一多，项目开始乱了。。。（doge）
Anthropic 透露，早期 Agent 虽然很快拿下了一些结果，但随着工程规模扩大，它们逐渐跟不上整个项目的状态，也越来越难有效协作。
这些失败尝试留下的代码，最终只占成品非模板代码的大约 7%。
真正的转折点，是团队换上了一个叫「Prove2Me」的平台——
这是 Tianyi Peng 及其哥伦比亚大学合作者专门为数学形式化搭建的一套协作系统。
我们可以把它理解成，给几十个 Claude 装上了一套数学版项目管理系统。
哪个定理已经证明了，哪个还缺前置条件，下一步该攻哪个节点，Agent 都能从这张图里判断。
同时，平台还会把定理陈述和证明分开管理、加速 Lean 编译，并给每个定理保留自然语言描述，方便不同 Agent 搜索和复用已有结果。
这一下，多 Agent 才真正开始像一支能协作的大型数学团队了～
而 Anthropic 最后使用的，则是 Prove2Me+ 基于 Claude Code 的 multi-agent harness。
最后整个项目消耗约 60 亿个输出 Token，内部使用的通用研究模型能力大致相当于 Claude Fable 5.1。
更夸张的是，人类在过程中提供的数学指导其实相当有限。。。
Tianyi Peng 更多只是偶尔给一些非常高层的提示，比如某个方向优先级更高、某个定理尽快推进。
剩下的大量定义、中间证明、任务拆分和拼装，主要由 Claude 自己完成。
负责审阅结果的 Kevin Buzzard 将其评价为一次「非凡的自动形式化成果」。
因为费马大定理的价值已经不止于又被 AI 证明了一遍——
如果这样规模、这样依赖复杂度的现代数学成果，都开始能够被 AI 自动搬进形式化系统，那么过去极度依赖人工、推进速度缓慢的数学文献形式化，可能第一次真正具备了大规模提速的条件。
One More Thing
Claude 这边刚用 11 天，把 350 多年的数学名题重「喂」给计算机验了一遍。
OpenAI 那边也没闲着，是的，GPT-6 Astra 开始往更多人手里塞了。。。
OpenAI 最新信息显示，GPT-6 Astra 正在逐步向 ChatGPT 付费用户开放。
其中 GPT-6 Pro 面向 Pro、Business 和 Enterprise 计划推出，Pro 用户还可以在 Chat、Work 和 Codex 里使用 Astra。
Sam Altman 也亲自出来吆喝了一波，大意很简单：
货到了，可以开始上桌了友友们～
长链路 Agent 任务、软件工程、计算机操作、浏览器使用，以及科学和专业工作。
A 社刚秀完 Claude 可以拉着一群 Agent，狠干 11 天数学工程。
OpenAI 转头开始把新旗舰往 Pro 和企业用户手里推。
我是感觉啊，一大批刚出炉的数学、科研和 Agent 狠活，估计已经跟着 GPT-6 Astra 一起在路上了。。。
参考链接：
[ 1 ] https://x.com/search?q=%E8%B4%B9%E9%A9%AC%E5%A4%A7%E5%AE%9A%E7%90%86&src=typed_query
[ 2 ] https://www.anthropic.com/research/formalizing-fermats-last-theorem
一键三连「点赞」「转发」「小心心」
欢迎在评论区留下你的想法！
— 完 —
点亮星标
科技前沿进展每日见
