AI都能验证费马大定理了，数学家还有啥用？

AI 用 11 天把费马大定理的证明翻译成了机器能逐行核验的代码。它 没有证明任何新东西 ，却把一个老问题重新摆上了台面。

9月4日，Anthropic发了一条公告。

Claude，用11天，完成了费马大定理的首个完整 形式化 证明。

数字堆在后面，一个比一个吓人。约1300万行Lean代码，相当于数学公共库Mathlib体量的5倍以上。3万多个定理，其中2.95万个中间定理被纳入最终证明。全程只用Lean的3条标准公理，没有一个未证明的占位符。

这项工作由Anthropic研究员彭天翼发起。他是清华姚班校友，此前和哥伦比亚大学的合作者一起开发过数学形式化协作平台。几十个Claude智能体在这个平台上协作，把这件事啃了下来。

数学界原本预计，人类完成它需要10年。

消息传开，惊叹和质疑一样多。而质疑里，藏着那个更大的问题。AI都这水平了，数学家还有什么用？

CHAPTER 01 · CLARIFICATION

先纠正一个误会

Claude没有证明费马大定理。

这颗358年的悬案，1995年就被英国数学家怀尔斯解决了。他在阁楼上秘密工作7年，1993年首次宣布，随后被同行发现漏洞，又修补了14个月，最终和理查德·泰勒一起发表了129页的证明。从那以后，费马大定理就是已证定理。

Anthropic做的是另一件事。怀尔斯那份证明，写给人看。人看一份129页的证明，靠 同行评议 ，靠信任，靠时间。而Claude把它转写成了机器能逐行核验的形式，每一行都由Lean这个证明助手检查过，中间3万个定理一个没跳。

这是一项非凡的自动形式化成就，AI的产物足够健壮，可以作为后续工作的基础。

—— 帝国理工数学家 Kevin Buzzard 评 Anthropic 公开的证明

但他同时指出了另一面。GitHub仓库里有106个上游文件，Claude依赖了大量前人搭好的数学基础设施。所谓11天，是从巨人肩膀上起跳的11天。

把话说得最直白的，也是Buzzard。这是自动形式化已有数学的成就，不产生任何新定理。

“把形式化包装成证明，就像把翻译一本外文书说成写了一本新书。翻译可以很有价值，但不是创作。”

这个类比值得每个关心AI的人记住。它划出了眼下最要紧的一条界线。

CHAPTER 02 · THE 50-YEAR DEBATE

这场架，数学界吵了五十年

机器碰数学的信任问题，不是第一次闹上台面。

1976年，阿佩尔和哈肯用计算机证明了四色猜想，听上去人畜无害的地图着色问题，成了第一个由机器完成的重大数学证明。

争议立刻爆发。《科学美国人》的封面直接宣告，证明之死。

哈肯的儿子后来在伯克利讲这段历史，说台下的听众分成了两派。

40 岁以上的人 不相信计算机的证明是对的VS40 岁以下的人不相信700 页手算是对的

这个分裂很有味道。它说明问题从来不在机器算得对不对，而在“过程我看不见，凭什么信”。

后来还有个更扎心的发现。有人复核那份证明，手工检查的部分，错误比机器检查的部分还多。人类的可检查，并不天然等于正确。

那场争论到1997年才缓和，一个更简洁的计算机辅助证明出现，机器也慢慢变成了数学家的日常工具。但哲学层面的疙瘩，五十年没解开。

这次费马大定理的形式化，是那场老争论的新回合。不同的是角色变了。1976年，计算机是计算器，人按键，它出结果。2026年，Claude是几十个自主协作的智能体，人只提供少量指导。

五十年前的问题是，机器算的算不算证明。五十年后的问题是，机器写的，还轮不轮得到人来检查。

KEY CHAPTER

发现、证明、验证，三段工作被切开

AI 吃掉的是第三段，纹丝没动的是第一段

01 发现→02 证明→03 验证

要看清数学家的位置，先把数学研究拆开。

一段是发现。提出猜想，找到新结构，看见别人没看见的关联。怀尔斯决定把职业声誉押在费马上，是在这一段。

一段是证明。把猜想变成定理，把直觉变成逻辑链。129页的证明，是这一段的产物。

一段是验证。检查证明对不对。传统上靠同行评议，几个专家花几个月，拿着放大镜逐行找漏洞。怀尔斯1993年的漏洞，就是这么被揪出来的，也差点毁掉整个成果。

AI这11天，吃掉的是第三段。

这件事的意义比听起来大。菲尔兹奖得主陶哲轩，过去几年一直在推Lean形式化，他的说法是，形式化带来 无需信任的协作 和“近乎即时的审稿”。两个互不相识、互不信任的数学家，可以在机器监督下合作，谁也别想蒙混过关。审稿从几个月，变成几分钟。

INSIGHT

把问题拆解成可处理的部分，这才是价值所在。

—— 菲尔兹奖得主 陶哲轩

顺着这个逻辑，第二段也在松动。形式化工具反过来帮人证明，菲尔兹奖得主里已经有六位在用Lean，陶哲轩自己用AI辅助推进过好几个项目。

纹丝没动的，是第一段。

他还警告过另一个趋势，开放问题像不可再生资源，一旦一个有价值的方向公开，大量AI算力可能迅速涌入，抢先推进。研究者可能因此不再公开有前景的方向，几百年的开放科学传统，可能被逆转。

这个警告换一面看，恰恰说明AI需要人来指方向。值得解的题，永远是稀缺的。

CHAPTER 04 · NEW ROLES

数学家的新位置

回到标题的问题。答案藏在重新分工里。

1

出题人

AI能在给定框架里疯狂推进，但框架本身，哪个问题值得问，哪条路有风景，还是人的判断。陶哲轩嘴里会枯竭的“不可再生资源”，换个角度看，就是出题人的身价在涨。

2

建筑师

1300万行代码，压在106个上游文件上。那些文件是人类几十年攒下的数学地基，Buzzard自己就领导过费马大定理的形式化社区项目。没有这一代代铺路，Claude无处起跳。数学家在变成给AI搭舞台的人。

3

监工

形式化不产生新数学，但它把“信”变成了计算。往后顶尖成果可能标配两份，一份人读的论文，一份机器验证的代码。谁来判断一份AI证明是金子还是垃圾？还是懂数学的人。

4

练新活的学生

北大的团队把Lean写进了给学生的指南，说它可以帮助百分之百验证证明的正确性。从小和证明助手一起长大的那批学生，数学训练的重心，可能会从“算对”挪向“问对”。

THE END

机器接管了苦役

所以，AI验证了费马大定理，数学家失去的是什么？

失去的是苦役。7年闭关里的孤独检查，129页证明里的逐行核验，审稿桌上几个月的放大镜。这些活，AI接过去了。

留下的，是怀尔斯在阁楼上做出那个决定的瞬间。

这个题值得押上7年，这条路可能有光。这样的判断，AI做不了。

数学这个行当最古老的那句话，此刻有了新注解。

CLOSING

机器接管了数学的苦役，剩下的部分，才更接近数学家这个职业的本义。