350 多年的岁月里，人类一直在寻找费马大定理的答案。
1637 年，法国数学家皮埃尔·德·费马在一本数学著作的页边写下一个困扰后世数百年的猜想，并留下了一句著名的话：「我发现了一个绝妙的证明，但这里的空白太小，写不下它。」
后来，人类真的找到了证明。1995 年，英国数学家安德鲁·怀尔斯花费多年时间完成了费马大定理的第一个完整证明。但如今，这个数学史上的传奇问题又迎来了新的节点。
官方博客 https://www.anthropic.com/research/formalizing-fermats-last-theorem
就在刚刚，Anthropic 公布了一项新的研究成果：Claude 在几乎自主运行的情况下，用 11 天完成了费马大定理的首个端到端计算机验证证明。
整个过程中，Claude 使用 Lean 编程语言构建形式化证明，生成约 1300 万行 Lean 代码，证明了超过 2.95 万个中间定理，最终得到了一份可以由计算机完整检查的证明。
这一次，AI 做的事情并非重新发现一个数学定理，而是完成了一项过去需要数学家多年投入的工作：把人类数学中的复杂证明，转换成计算机能够逐步验证的形式。
哦，对了，伴随着 GPT-6 Astra 的全面开放，Anthropic 刚刚也给 Claude 用户送上了一份「大礼包」——重置了所有 Claude Max 用户的每周使用额度。
一道数学难题，困住了人类 3 个世纪
费马大定理的问题本身非常简单。
当 n 大于 2 时，是否存在正整数 a、b、c，使得 aⁿ+bⁿ=cⁿ？
费马认为不存在这样的解。
然而，这个看似简单的问题，却成为数学史上最著名的难题之一。
过去几个世纪，无数数学家尝试证明它。1908 年，德国哥廷根科学院甚至为解决费马大定理设立了高额奖金，仅第一年就收到 621 份错误证明。
直到 1995 年，怀尔斯才正式发表被数学界认可的证明。
不过，怀尔斯的证明远比普通数学问题复杂。
整篇论文超过 100 页，涉及现代数论、代数几何等多个数学领域。1993 年，怀尔斯首次公布证明后，评审团队在验证过程中发现关键漏洞，他随后花费一年时间修正，最终才完成最终版本。
这件事也暴露了现代数学中的一个长期问题。
证明一个数学定理很难，验证一个复杂证明同样困难。
数学论文通常面向人类阅读，很多显而易见的推导不会逐步展开。但计算机不会默认任何步骤，每一个逻辑关系都必须被明确表达。
因此，数学界开始探索另一条道路：形式化证明。
通过 Lean 等证明助手，数学家可以把数学推理转换成计算机语言，让计算机自动检查证明中的每一个环节。
过去几年，数学界一直尝试将费马大定理形式化。
2024 年，伦敦帝国理工学院数学家 Kevin Buzzard 发起相关项目，希望利用 Lean 完成这一任务。
按照当时的估计，这项工作可能需要多年时间。
因为怀尔斯的证明建立在几百年的数学积累之上，而计算机能够直接理解的数学知识，只占整个数学体系的一小部分。
数学家需要先将大量基础理论转换为形式化语言，再逐步搭建整个证明体系。
这是一项庞大的数学工程。而 Claude 的出现改变了推进速度。
证明很难，证明证明更难
这项工作的背后，是一位长期探索 AI 与数学交叉领域的研究者。
Tianyi Peng（彭天翼）是此次费马大定理形式化项目的重要推动者。
他本科毕业于清华大学姚班，随后在麻省理工学院完成博士研究，目前担任哥伦比亚大学商学院助理教授，同时也是 Anthropic 研究员。
他的研究方向长期围绕 AI Agent、强化学习以及数学形式化展开。
此前，他与哥伦比亚大学团队共同开发了 Prove2Me 平台，希望通过多智能体协作，让 AI 能够参与更复杂的数学证明任务。
这项研究背后还有一个颇具意味的经历。
在本科阶段，Tianyi Peng 曾完成一项数学研究成果，导师希望将相关结果纳入 Nature 论文。但面对导师提出的一个问题：「你是否确定这个证明完全正确？」他的回答是：「我有 99% 的把握，但这么长的证明很难做到 100% 确定。」
最终，这项成果没有进入 Nature。
多年后，他选择研究数学形式化，某种程度上正是在解决当年遇到的问题：如何让复杂数学证明拥有更可靠的验证方式。
Tianyi Peng 希望测试 Claude 是否能够帮助推进费马大定理的形式化。
让人意想不到的是，结果大大超过了预期。
在 11 天时间里，Claude 基本自主完成了整个证明流程。为了处理如此复杂的任务，Anthropic 并没有让单个 AI 直接完成全部工作，而是让多个 Claude Agent 协同合作。
这些 Agent 分别负责定义数学概念、证明中间定理，并利用已经完成的结果继续推进后续证明。
最终，Claude 生成了约 1300 万行 Lean 代码。
这个规模远超普通数学形式化项目，相当于 Lean 最大数学库 Mathlib 规模的 5 倍以上。
整个过程中，Claude 构建了约 3.03 万个定理，其中最终证明费马大定理使用了约 2.95 万个中间定理。
为了管理如此庞大的证明过程，Anthropic 使用了一个名为 Prove2Me 的开放协作平台。
这个平台能够帮助 AI Agent 管理不同数学任务之间的关系，将复杂证明拆分成多个可以并行推进的小目标，同时记录每个定理之间的依赖关系。
结合 Claude Code 的多 Agent 工作方式，研究团队最终在不到两周时间内完成了整个形式化证明流程，总共消耗约 60 亿输出 token。
最终结果通过 Lean 检查，只依赖数学基础公理，没有额外假设。
未来的数学家，可能需要同时面对人和 AI
Claude 完成费马大定理形式化证明的意义，并不只是速度提升。
过去，数学研究依赖同行评审确认结果是否正确。但面对越来越复杂的数学成果，人工验证正在变得越来越困难。
历史上，数学界曾多次经历漫长验证过程。
1998 年，托马斯·黑尔斯证明开普勒猜想，评审团队花费多年时间审核，最终只能给出高度可信的评价。
2002 年，佩雷尔曼提出庞加莱猜想证明，数学界同样花费多年时间整理和确认。
随着 AI 开始参与数学研究，这个问题可能更加突出。未来，AI 或许能够快速生成大量数学证明，但人类研究者很难逐一阅读和验证。
形式化证明提供了一种新的可能。AI 可以负责生成证明，人类负责理解思路，而 Lean 等系统负责检查逻辑正确性。
Anthropic 认为，未来数学论文可能会同时包含面向人类阅读的解释，以及面向计算机验证的形式化证明。
这不会取代数学家的创造力，但会改变数学成果被验证和传播的方式。
过去，数学家的工作重点是提出新的理论。未来，他们可能还需要考虑如何让这些理论能够被机器理解和验证。
389 年前，费马在页边留下了那份属于人类直觉的骄傲与遗憾。
而在 389 年后的今天，这片曾经狭窄的空白，终于被人类亲手创造的 AI 数字工具，填上了一份最工整、最确凿的答案。
我们正在招募伙伴
简历投递邮箱hr@ifanr.com
✉️ 邮件标题「姓名+岗位名称」（请随简历附上项目/作品或相关链接）
热门跟贴