克劳德帮助完成了费马大定理的第一个形式化证明

Anthropic 的 AI 模型验证了超过 29,500 个定理，生成了数学最著名的证明之一的机器检查版本

1637 年，皮埃尔·德·费马 (Pierre de Fermat) 在一本数学教科书的页边空白处写下了一条注释，声称他的证明太大，无法在空间中容纳。人类花了 358 年才真正证明他是对的。现在，人工智能已经做了一些可以说更难的事情：将证明翻译成计算机可以逐行验证的语言，且歧义为零。

Anthropic 的 Claude 使用 Lean 4 生成了费马大定理的第一个完整的机器检查形式化，Lean 4 是一个证明助手，其功能就像一位残酷诚实的数学老师，拒绝让你跳过任何步骤。形式化涵盖了超过 29,511 个定理和 1,450 个定义，全部通过 Lean 内核进行验证，而不依赖于标准 Mathlib 基础之外的公理。

形式化实际上意味着什么

安德鲁·怀尔斯 (Andrew Wiles) 于 1995 年证明了费马大定理，数学界也接受了它。但数学上的“接受”仍然为人为错误留下了空间。形式化证明是不同的。每个逻辑步骤都用专为数学推理设计的编程语言进行编码，并且计算机独立地检查每个步骤。

克劳德的形式化遵循弗雷曲线和模块化提升方法，这是怀尔斯和泰勒开创的现代路线。这与 Kummer 的经典方法不同，后者仅处理所谓的“正则素数”，并不涵盖完整的定理。这项工作记录在 Anthropic 的公共 GitHub 存储库 anthropics/fermats-last-theorem 中，任何人都可以在其中检查完整的证明链。

多年的人类基础使这成为可能

将这一切完全归功于克劳德，就像将发现美洲归功于全球定位系统一样。这种形式化建立在交互式定理证明社区多年的努力之上，其中最著名的是 Kevin Buzzard 在伦敦帝国理工学院正在进行的项目。

巴扎德是一位纯数学教授，多年来一直致力于将精益的主要数学结果形式化。他的 FLT 形式化项目预计将至少持续到 2029 年，这反映出即使由人类数学家推动这一过程，这项任务也是多么艰巨。

预计在 2024 年或 2025 年发表的另一篇学术论文将首次对 FLT 正则素数案例进行完整的精益形式化。这项工作是并行进行的，使用库默的旧方法解决同一定理的不同部分。

Claude 的贡献是该社区的基础工作与 Anthropic 推动人工智能适用于严格推理任务的交叉点。人工智能在最少的人类监督下生成并验证了复杂的精益证明，但它是在数学家花费数年时间构建的脚手架上完成的。

为什么这比数学更重要

费马大定理指出，对于任何大于 2 的 n 值，没有三个正整数 a、b 和 c 可以满足方程 a^n + b^n = c^n。Wiles 的原始证明长达 100 多页，几乎借鉴了现代数论的每个主要分支。

将其压缩为机器可验证的逻辑（超过 29,500 个单独的定理）是对人工智能推理的压力测试，远远超出了典型的基准。大多数人工智能评估涉及多项选择题或简短的问题解决。这需要在数千个相互依赖的步骤中进行持续的、结构化的逻辑推理。

对于数学界来说，这加速了长期愿景的实现：每个主要定理都有一个任何人都可以审核的机器检查证明。巴扎德多年来一直直言不讳地表达这一目标，认为非正式证明无论被多么广泛地接受，都存在包含细微错误的非零风险。

克劳德所取得的成就与完全自主的数学发现之间的差距仍然很大。形式化现有的证明，即使是如此复杂的证明，也与发现新的证明有着根本的不同。更难争论的是输出：精益内核接受的证明，涵盖了数学史上最著名的结果之一的每一个逻辑步骤。