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