Anthropic宣布AI模型11天完成费马大定理首个机器验证证明
Anthropic于2026年9月4日宣布，其AI模型Claude仅用11天完成了费马大定理的首个端到端机器验证证明。整个过程中，Claude编写了1300万行代码，产出30300条可验证定理，其中29500条被最终证明采用，累计消耗60亿Token。这是迄今为止规模最大的Lean证明。
费马大定理由法国数学家费马于1637年提出，困扰数学界超过350年，直到1995年才由英国数学家怀尔斯给出证明，相关论文长达129页。由于证明极为复杂，将其形式化为机器可验证的代码此前被数学界视为以年为单位的超级工程。
在此次项目中，Anthropic的研究团队采用了多智能体协作方式，几十个Claude智能体在Prove2Me平台上并行工作，通过定理任务树、自然语言索引等机制分工证明中间定理，最终在Lean编译器中通过全部检查，仅依赖三条基础公理。Anthropic表示，该成果标志着大规模自动形式化在数学领域的工程化落地迈出重要一步。
此外，Anthropic还透露，团队用3个普通账号在Prove2Me上花费3天时间，就完成了数论中维诺格拉多夫三素数定理的形式化验证，显示该工具进一步降低了数学验证的门槛。
- 2026-09-08 16:39 | 36氪：11天、30万美元：AI攻破358年数学难题的最后一关阅读原文
近日，Anthropic宣布了一项震动数学界的消息：其AI模型Claude在基本自主运行11天后，完成了费马大定理的首个端到端、可由计算机完整检查的形式化证明。 这不是AI第一次在数学领域引发轰动。但这一次，震撼程度完全不同。 一个350年的“页边空白” 故事要从1637年说起。 法国数学家皮埃尔·德·费马在一本数学书的页边潦草地写下了一句话：对于任意整数n>2，不存在正整数a、b、c使得aⁿ+bⁿ=cⁿ。他还补了一句——自己有一个“真正绝妙的证明”，可惜页边太窄写不下。 然后他去世了。 接下来358年，一代又一代数学家前赴后继，试图找回费马口中那个“绝妙证明”。欧拉、...
- 2026-09-04 18:16 | 36氪：刚刚，Claude首次证明费马大定理，清华姚班大神出手了阅读原文
就在刚刚，数学圈又有惊人消息。 清华姚班大神带队，用Claude彻底攻克了费马大定理。 至此，AI完成了数学史上最大证明。 曾经，费马大定理折磨了人类350多年，需要数学家耗费数年心血，写下129页天书才能证明。 今天，Anthropic却宣布，Claude仅用11天，就完成了费马大定理的首个端到端机器验证证明！ 为此，Claude疯狂敲了1300万行代码，产出了30300条可验证定理，最后有29500条被采用，直接进了最终证明。 这个体量，是全球最大数学定理库Mathlib的5倍还多！而且，整个过程烧掉了足足60亿Token。 这是迄今为止编写的最大的 Le...