Claude 在 Lean 中形式化了费马大定理

Anthropic 宣布了由 Claude 产生的第一个完整的、经过计算机检查的费马大定理 (FLT) 证明。在长达 11 天的自主工作中，该 AI 系统编写了 1300 万行 Lean 代码，并证明了 29,500 个中间定理，从而实现了一个数学界原本预计需要数年才能完成的形式化结果。

取得的成就：FLT 的自动形式化

Claude 对费马大定理的形式化是自动形式化（autoformalization）过程中的一个重要里程碑——即通过将人类可读的数学推理转换为计算机可以进行算法验证的形式的过程。

该项目的关键技术指标包括：

时间线： 11 天的自主工作。
规模： 1300 万行 Lean 代码，其规模是 Mathlib（Lean 的主要社区库）的五倍以上。
复杂度： 总共证明了 30,300 个定理，其中 29,500 个用于最终证明。
资源消耗： 来自一个与 Claude Fable 5.1 相当的内部研究模型的约 60 亿个输出 token。

该证明遵循了 Andrew Wiles 在 1995 年证明的简化版本，特别是 Darmon, Diamond, and Taylor 的阐述。它仅依赖于 Lean 的三个标准公理，并通过比较器验证与 Mathlib 对 FLT 的陈述一致。

通过 Prove2Me 克服验证挑战

形式化复杂的证明是困难的，因为像 Lean 这样的证明助手要求每一个逻辑步骤都必须是显式的，而人类的证明往往会跳过“显而易见”的步骤。为了管理这种复杂度，Anthropic 利用了 Prove2Me，这是一个由 Tianyi Peng 和哥伦比亚大学的合作者设计的开放协作平台。

Prove2Me 通过三个主要机制实现了项目的成功：

有向无环图 (DAG) 管理： 该平台维护定理陈述的 DAG，允许多个智能体并行工作，并通过提供清晰的“下一步证明什么”的路线图来减轻内存退化问题。
优化编译： 通过将定理陈述与其证明分别存放在不同的文件中，系统减少了 Lean 的编译时间和资源消耗。
自然语言索引： 每个定理陈述都附带了自然语言描述，这有助于在智能体团队中进行搜索和复用。

对数学研究的影响

这一结果表明，AI 现在可以形式化现有数学文献的大部分内容，这对该领域的严谨性和验证工作具有直接影响。

减轻同行评审的负担

传统上，验证一项新颖的数学结果可能需要数月或数年。自动形式化可以减轻人类评审员的负担，并为检查 LLM 生成的数学提供一种严谨的方法，而这目前是一个成本高昂的人力驱动过程。

增强 AI 自身的推理能力

Anthropic 指出，编写 Lean 代码有助于 Claude 证明新颖的结果。通过在发现证明的同时进行形式化，AI 可以独立地检查自己的假设，类似于研究人员使用数值模拟来验证研究方向。

社区观点与批评

虽然这一成就被伦敦帝国学院的 Kevin Buzzard 称为“非凡”的，但该项目在技术社区中引发了关于证明性质的广泛讨论。

对“面条式代码”的担忧

一些批评者认为，如此庞大的代码量（1300 万行）表明该证明可能效率低下，或者缺乏人类数学家所追求的可复用抽象。

一位评论者指出：

This is quite useless actually. The whole point of formalizing FLT was to clean up modern number theory into reusable abstractions... If its 13 million LoC, it might involve so much spaghetti that its unusable other than the result.

对验证器的信任

人们提出了疑问，AI 是否可能利用了 Lean kernel 本身的潜在漏洞。由于证明非常庞大且由 AI 生成，一些用户质疑了“谁来验证验证器”的问题，建议使用像 Metamath 这样更小的 kernel 来处理如此大规模的输出。

暴力破解式自动形式化的社会价值

对于“暴力破解”式的自动形式化是否能提供与人类主导的形式化具有相同的价值，目前存在争议。一些人认为，通过大规模 token 消耗和智能体规模化来解决著名问题，AI 实验室可能会削弱人们进行创造人类可理解的形式化库的艰苦工作的动力。