Anthropic 利用 Claude 以史无前例的方式将费马大定理“形式化”，但编写仍需 11 天
- Claude 将著名数学证明转化为数百万行可验证的代码
- Anthropic 称，原本预计需要数年才能完成的工作，Claude 仅用了 11 天
- 该庞大的证明包含 1300 万行 Lean 代码
Anthropic 利用其 Claude 人工智能系统，生成了一个完全由计算机验证的、源自数百年前著名数学证明的版本。
该证明涉及费马大定理。这一假设最早由数学家皮埃尔·德·费马于 1637 年提出。
数学家安德鲁·怀尔斯早在 1995 年就给出了该定理的完整数学证明，全文长达 129 页。
Latest Videos FromTechRadar在此观看完整视频：为机器重构的证明
形式化证明，简单来说就是将数学推理转化为代码，让计算机无需人工协助即可自动进行检查。
根据数学家最初对该项目的描述，Anthropic 表示，他们原本预计整个任务需要几年时间。
然而，该公司称其内部研究模型仅用 11 天连续且基本无监督的工作就完成全部证明。
最终完成的证明由 1300 万行专门代码组成，使用的是数学家常用的 Lean 编程语言。
据报道，在这一过程中，Claude 的智能体证明了大约 30,300 个独立的定理，最终在版本中采用了其中 29,500 个。
在整个十一天的过程中，人类的参与仅限于偶尔提供高层指导，并未进行任何直接的手动编码。
这份 1300 万行的证明篇幅，是社区主证明库 Mathlib 的五倍以上。
帝国理工学院数学家 Kevin Buzzard 评价道：“这一非凡的自动形式化成果……在没有除公理之外任何其他假设的前提下，证明了费马大定理。”
“在此期间，我们还见证了对代数、调和分析、几何和数论的自动形式化。我们认识到，AI 自动形式化的成果已经足够稳健，可以作为后续工作的基础；该证明具有多层次结构。”
Anthropic 在成功之前尝试了多次形式化，这些尝试大约贡献了最终证明中 7% 的非模板代码行。
这并非 Anthropic 首次取得数学突破
就在一个月前，Anthropic 才公布过另一项突破，与黎曼 ζ 函数这一被广泛研究的数学对象有关。
该函数正处于黎曼假设的核心，而黎曼假设被认为是全球数学界最难的未解难题之一。
竞争对手 OpenAI 也在推进类似的工作，用最新的 Astra 模型解决了多个经典的 Erdős 问题。
据报道，OpenAI 的这项工作还缩小了理论计算机科学领域多个悬而未决的长期问题的范围。
Anthropic 表示，这次突破是在让 Claude 使用一款名为 Prove2Me 的开源软件工具之后才实现的，该工具由外部合作者开发。
这款软件能帮助 AI 智能体在漫长的多阶段研究流程中选出最有用的下一步行动，同时还能降低推理成本。
Anthropic 还扩大了面向数学家的免费额度与研究资助，专门支持从事形式化项目的研究者，并提供更大规模的专项资助。
尽管这次刷新了速度纪录，但 11 天的耗时依然表明：即便使用当今最强大的系统，完整的形式化仍然是一项极其耗费人力的工作。
