Anthropic 团队最近公开了一项研究：他们用 Claude 在 11 天内完成了费马大定理在 Lean 语言中的端到端形式化证明。

这项研究意味着，用机器对现代前沿数学进行大规模、端到端的机器可验证重构，已经进入了工程可行的阶段。

要理解这件事的意义，得先看现代数学究竟遇到了什么麻烦。

1995 年安德鲁·怀尔斯彻底证明费马大定理时，交出的是长达 129 页、融合了椭圆曲线、模形式与伽罗瓦表示的庞大体系。然而真正的考验在论文写完之后才刚刚开始：如何证明这个证明是对的？

当时全世界能完整审阅这套推导的学者屈指可数。几位顶尖数学家组成的评审团花了两个多月逐行核验，依然在第三部分挖出了一个致命漏洞；怀尔斯随后与理查德·泰勒闭关修补了一整年，才终于把逻辑链条闭合。

这就是现代数学日益严峻的验证危机。理论越来越深，交叉工具越来越繁复，而人类大脑处理超长、高密度逻辑链的能力是有限的。

为了摆脱对人类评审主观精力的依赖，数学界近些年转向了形式化证明（Formal Verification）。比如用 Lean 这样的交互式定理证明器，把自然语言写就的论文，翻译成计算机能逐行编译的代码。

形式化的门槛极高。人类写论文习惯用“显然可知”、“同理易证”略过繁琐细节，但 Lean 的内核不讲人情，任何推导都必须严格回溯到底层公理，跳过半步就会报错。此前数学界普遍认为，把怀尔斯整套证明完全形式化，需要数十位顶级专家全职投入数年时间。

而这次的多 Agent 系统只用了 11 天。

翻看他们开源的代码库，这几乎是一场纯粹的工程推进：数十个智能体协同推导了近三万个中间引理，生成了 1300 万行 Lean 代码，相当于 Lean 官方核心数学库（Mathlib）体积的数倍。整份证明没有留下任何用于跳过步骤的 `sorry` 占位符，且通过了独立的 Rust 验证内核交叉检验。

但这并不是单纯把大模型丢给编译器就能跑出来的结果。

研究团队在报告中写得很坦诚：如果直接让模型接手长程证明，随着上下文拉长和记忆衰减，智能体会迅速陷入幻觉和无效循环。

真正解决问题的是哥伦比亚大学团队构建的调度框架 Prove2Me。他们用有向无环图（DAG）把怀尔斯的宏大证明拆解成数万个细粒度的局部引理节点。模型不再需要统揽全局，它只负责在明确的上下文约束下，完成“从 A 和 B 推出 C”的微观推演；宏观的图谱拓扑与探索方向，则由人类研究员设定规则和适时纠偏。

大模型的局部符号推理能力，在严密的软件工程架构下被充分释放了出来。

这件事最值得关注的，其实是它对未来科研范式的提示。

人们常说大模型在严肃科学里最大的软肋是“幻觉”。但在形式化证明的语境下，编译器成了绝对客观的裁判。不管推理过程有多跳跃，只要代码能通过严格的类型检查与内核验证，结论就是严丝合缝的。

当繁重、枯燥的逻辑查漏与底层推导能够交由机器批量完成，人类学者的精力将被进一步解放到宏观猜想、理论建构与跨领域直觉的探索上。

1637 年，费马在《算术》的页边写下那句著名的断言：“这道空白太小，我写不下它的美妙证明。”

三百八十多年后，数以万计的细碎推导与千余万行代码被送入编译器，终于在数字世界里，把那道狭窄的空白填补得毫无缝隙。

【参考资料】

Formalizing Fermat's Last Theorem. Anthropic Research. (2026).

Chen, S., Marwaha, K., Lu, X., Yuen, H., & Peng, T. (2026). Prove2Me: An Open Collaborative Platform for Scaling Math Formalization. _arXiv preprint arXiv:2608.28433_.