Claude 完成费马大定理首个形式化证明

哥伦比亚大学商学院助理教授彭天翼利用 Claude，在 11 天内以高度自主的方式完成了一项被描述为费马大定理第一个完整且经计算机检验的形式化证明。该证明使用 Lean 编程语言编写，共生成 1300 万行代码，并证明了 29500 个中间定理。

这项工作采用 Prove2Me 平台。平台通过维护定理陈述的无环图（DAG）组织证明结构，并使用多智能体协作推进长链推导。材料指出，这种设计有效克服了单一智能体在复杂逻辑推导中容易出现的资源损耗与协作失效问题。

从工程实现角度看，DAG 状态管理和多智能体任务分解可以借鉴到复杂软件验证、长流程自动化等场景。AI 生成形式化证明也可能推动 Lean 工具链在开发测试阶段的应用，帮助团队在早期发现逻辑缺陷。

这一成果同时展示了 AI 自动形式化现代数学文献的可行性。对数学家而言，它可能用于辅助校验研究成果、规避错误，从而减轻评审新证明的压力。不过，这仍是基于本次工作的可行性判断，实际效果需要通过更多独立复现来检验。

目前公开信息尚未说明 Prove2Me 平台是否公开可用、安装方式与许可证，也未披露 Claude 的具体模型版本、调用方式、人工干预程度、计算资源消耗与时间开销。该证明是否已经独立评审或被 Lean 社区接受，同样有待后续确认。