Claude AI耗时11天完成费马大定理机器证明，被称为迄今为止最长的数学证明
Anthropic公司宣布,其内部一个大致相当于Claude Fable 5.1水平的研究版本模型,用11天时间完成了对"费马大定理"的完整形式化证明,生成代码总量达1300万行Lean语言代码,被称为迄今为止最长的数学证明。
费马大定理由法国数学家皮埃尔·德·费马于1637年提出,该定理表述为:当整数n大于2时,不存在使aⁿ+bⁿ=cⁿ成立的正整数解;这一猜想在提出358年后,由英国数学家安德鲁·怀尔斯于1995年首次给出严格数学证明,论文长达129页。
Anthropic此次并非做出新的数学发现,而是将怀尔斯原有证明进行"形式化"处理,即用可被计算机逐行验证的Lean证明助手语言重新表述并核验整个证明链条,过程中共验证30,300条中间定理,其中29,500条最终被纳入完整证明,整个任务消耗约60亿个输出token。
该项目使用名为"Prove2Me"的调度工具,以有向无环图结构管理各条定理之间的依赖关系,由数十个Claude智能体并行协同工作,并将定理陈述与具体证明过程分离处理以提升编译效率;项目负责人为Anthropic研究员彭天异(Tianyi Peng,与哥伦比亚大学合作),项目建立在英国帝国理工学院数学家凯文·巴泽德(Kevin Buzzard)此前发起的费马大定理形式化项目基础之上,并调用了社区维护的数学形式化库Mathlib及非营利组织Lean FRO的相关基础设施,GitHub提交中引用了106个上游文件。
巴泽德在审阅后确认该证明"除数学公理本身外不依赖任何其他假设",另有比对工具确认该证明所陈述的定理表述与Mathlib官方版本一致;完整证明已上传至GitHub供外界独立复核,巴泽德将其称为"历史性时刻(有待复核确认)"。
该形式化工作于2026年8月7日至18日期间完成,历时11天;文章同时提到,此前由巴泽德在帝国理工学院牵头的人工形式化费马大定理项目自2024年启动以来仍未完成,而最终生成代码中约有7%属于此前尝试失败或重复的部分。
来源：公开信息
ABAB AI 解读
Anthropic此次并非首次将Claude用于攻克数学难题——今年7月,该公司研究团队已披露Claude(彼时称为Fable 5)协助解决了存在87年的一道数学猜想,随后又有诺贝尔奖得主物理学家团队使用Claude解出存续数十年的数学难题;这次费马大定理形式化项目,延续了Anthropic今年以来持续释放"Claude具备顶尖数学研究能力"信号的一贯节奏,也与OpenAI、DeepMind此前分别在国际数学奥林匹克竞赛和几何定理证明上高调展示模型能力的路径相似。
这类数学证明类展示的直接商业价值有限,但资本意义在于为模型能力建立可验证、难以造假的"硬指标"背书——相较于跑分和用户评测,数学形式化证明这类可由独立学者(如巴泽德)公开核验的成果,更能取信于机构投资者和企业客户,Anthropic借此强化其在"高价值推理任务"上对OpenAI、Google DeepMind的差异化定位,为后续在企业级科研、金融建模等高端市场的定价谈判积累信任资产。
这与DeepMind旗下AlphaProof、AlphaGeometry此前在数学竞赛题上取得金牌级表现的路径同属一条能力展示曲线——通过在人类公认高难度、可客观验证的智力任务上取得突破,来对外证明模型推理能力已进入新阶段;当前大模型行业正处于从"聊天助手"向"科研协作工具"扩展应用边界的阶段,数学形式化证明恰好是这一转型中最容易被专业社群客观核验、也最不容易被质疑"刷榜"的展示场景。
本质上属于"技术替代"——机制层面,传统数学证明的形式化验证过去需要数学家团队耗费数年人工逐行核对(如巴泽德团队自2024年启动、至今仍未完成的同类项目),而Claude通过数十个智能体并行处理、结合有向无环图式任务调度,将原本以"人年"计的工作压缩到11天完成;这标志着形式化验证这类高度依赖大量重复性逻辑核查的数学劳动,正率先被AI大规模替代,而人类数学家的核心价值将进一步集中到提出新猜想、设计证明思路等原创性判断环节。
ABAB News · 认知定律
能被独立核验的成果,比能被刷出来的分数更值钱。
机器替代的永远是重复核查,留给人类的永远是提出问题。
11天完成的形式化,买的不是数学突破,是能力信任。