Claude完成费马大定理首个端到端机器验证证明

会懂网AI资讯，9月5日，Anthropic宣布，Claude在基本自主运行11天后，完成了费马大定理首个端到端、经计算机检查的形式化证明。该工作由清华姚班校友Tianyi Peng团队主导，消耗约60亿输出Token，产出29500条被采纳定理，代码量超1300万行，为Mathlib规模的5倍以上。

费马大定理是数学史上最具标志性的难题之一，1994年由安德鲁·怀尔斯证明。此次Claude以机器可验证的形式化方式重新完成证明，意味着AI不仅能”生成看似合理的数学论证”，而是能产出经过计算机严格校验的证明。
形式化证明的价值在于”零歧义”：每一步推理都被机器检查，杜绝了人为疏漏。Claude在11天内产出1300万行代码、29500条定理，其规模远超现有数学库Mathlib的5倍，展现出AI在长周期、高强度数学推理上的惊人耐力。
这一成果的意义不仅在于数学本身，更在于它验证了AI”自主长期科研”的能力边界。过去AI参与科研多是辅助性的，而此次Claude在基本自主的情况下持续推进一个宏大证明，显示出AI正从”工具”向”科研协作者”乃至”独立研究者”演进。
Anthropic还开源了相关Lean 4代码，供社区复现与审查。这种开放态度，既是对成果可信度的背书，也为形式化数学与AI的结合提供了可复用的基础设施。
会懂网观察，Claude完成费马大定理的机器验证，是AI迈向”数学与科研自动化”的一个里程碑。当AI能够在11天内产出超越人类单个团队数月乃至数年工作的形式化证明，科学研究的方法论本身，正在被深刻改写。