Claude完成费马大定理首个完整形式化证明
本条为 AI 依据下方公开信源自动整理生成的摘要，不构成转载，可能存在偏差，请以原文为准。整理者：贝果科技 AI 资讯助手。
全文梳理
AI 摘要依据下方信源原文自动整理，非原文转载把人类证明译成机器可查
这次工作的对象并非费马大定理本身，而是把数学家已经接受的证明改写成Lean能逐行核验的形式。Lean在这里承担的是检查器角色：定理、定义与推导步骤都要写成它认可的写法，每一步是否从既有公理和定理合法推出，由程序判定，不接受「此处显然成立」这类跳过。产出规模约为1300万行Lean代码，涉及超过3万个中间定理，最终证明调用其中约29500个。作为参照，这一体量达到Lean核心数学库Mathlib的五倍以上。Anthropic方面说明，完整证明只依赖Lean的三个标准公理，并用比较程序核对过，Claude最终证明的定理陈述与Mathlib中的费马大定理一致，因此结论不依赖模型自述完成。
多智能体并行与分工
执行方式是把不同Agent同时拉起，各自承担不同环节：有的补齐数学定义，有的专攻中间引理，有的沿已有结果向更高层定理推进，还有的负责把分散部分重新拼回整体证明体系。项目由Anthropic研究员Tianyi Peng发起，他最初只想测试Claude能把这件事推进多远，结果一路做到终点。人类提供的数学指导相当有限，多为高层提示，例如某个方向优先级更高、某个定理尽快推进；大量定义、中间证明、任务拆分与拼装由Claude自行完成。审阅结果的Kevin Buzzard将其称为一次非凡的自动形式化成果。整个项目消耗约60亿个输出Token，内部所用通用研究模型能力大致相当于Claude Fable 5.1。
协作平台与流程约束
早期多Agent协作很快遇到规模扩大后的状态跟踪与配合难题，失败尝试留下的代码最终只占成品非模板代码的约7%。转折来自换用Prove2Me平台，这是Tianyi Peng与哥伦比亚大学合作者为数学形式化搭建的协作系统。它把整个证明拆成由定理节点组成的有向无环图，哪个定理已证、哪个还缺前置条件、下一步该攻哪个节点，Agent都能从图中判断；平台还把定理陈述与证明分开管理，加速Lean编译，并为每个定理保留自然语言描述，便于不同Agent检索和复用已有结果。最终采用的是Prove2Me加上基于Claude Code的多智能体harness。
与既有形式化计划的差别
此前数学界的路径是按多年社区工程来准备的：2000年代已有计算机科学家提出形式化Wiles证明的设想，2024年帝国理工学院Kevin Buzzard等人正式启动使用Lean完成费马大定理形式化的项目，仅第一阶段的技术蓝图就写了86页。此次Claude用11天走完全程，差别主要体现在工程量而非数学发现上——它没有给出一个全新的费马大定理证明，而是把可读证明完整翻译为可机器检查的形式。适用范围也由此明确：成果的价值在于逻辑检查层面的端到端可核验，读者可以把它理解为一次大规模自动形式化的工程实践，其规模、耗时与依赖公理数量均可对照上述数字自行判断。
为什么值得看
展示AI在复杂数学形式化证明上的突破性进展，为AI辅助数学研究开辟新路径。
信源1 家
关键事实
相关 · 论文
本页内容由 AI 自动聚合公开信源生成，仅供了解行业动态参考，不构成任何投资或决策建议。如需引用请以原文出处为准。