形式化费马大定理：AI在11天内完成计算机验证

项目背景

费马大定理（FLT）是数学史上最著名的猜想之一：对于任何大于2的整数n，方程aⁿ + bⁿ = cⁿ没有正整数解。该定理由皮埃尔·德·费马于1637年提出，但直到1995年才由安德鲁·怀尔斯给出完整证明，证明长达129页。此后，数学家们一直尝试将这一复杂证明形式化，即转换为计算机可自动检查的逻辑形式。2024年，伦敦帝国理工学院的Kevin Buzzard发起了使用Lean证明助手形式化FLT的社区项目，预计需要多年时间。

形式化过程

Anthropic研究人员Tianyi Peng决定测试其AI模型Claude能否加速这一过程。Claude在11天内（几乎全自主）完成了端到端的计算机验证证明。期间，它撰写了1300万行Lean代码，证明了29500个中间定理。最终证明仅使用Lean的三个标准公理，并通过比较器确认其陈述与Mathlib库中FLT的表述一致。

证明的编写采用了多智能体协作框架：数十个Claude智能体分工定义概念、证明中间定理，并逐步攻克更难的命题。初始尝试中，智能体常因记忆退化而丢失项目状态，导致协作失败。切换到由Peng及其合作者开发的开放平台Prove2Me后，问题得到解决。该平台通过维护有向无环图（DAG）跟踪定理状态，分离定理陈述与证明文件，并维护自然语言描述，有效支持了并行编译和搜索复用。

验证方法

传统数学证明依赖人类评审，过程可能耗时数月甚至数年，且容易遗漏错误。形式化证明则通过Lean等证明助手逐行检查逻辑，确保每一步都严格正确。Claude的证明遵循了简化版的怀尔斯证明（依据Darmon、Diamond和Taylor的阐述），并复用了部分已有形式化成果（如Imperial College项目及flt-regular项目）。人类仅提供少量高层指导，例如“Jacobian作为方案优先级高”、“推动Mazur定理尽快完成”。

意义与影响

该成果是形式化数学领域的里程碑。Kevin Buzzard评价称：“如果自动形式化FLT现在成为可能，那么我们就向自动形式化现代数学文献迈出了一大步。”这种技术将有助于发现数学文献中的潜在错误，减轻评审负担，并能够严格检查AI生成的数学结果。随着AI生成定理的数量激增，附带形式化证明将成为一种标准做法，帮助人类保持对数学知识体系的信任。

此外，实验表明，即使使用消费级AI订阅（如Claude Max），通过Proper2Me平台，多个智能体也能在数天内完成如维诺格拉多夫三素数定理的形式化。Anthropic已扩大对外部研究者（包括数学家和形式化专家）的免费或折扣订阅支持，并设立专项资助，用于形式化其他重要定理或改进Lean和Mathlib。

结论

形式化费马大定理表明，AI可以高效完成极其复杂的数学验证工作。这不仅是技术上的胜利，也为数学研究带来了新的可能性：数学证明的验证将变得更加可靠和高效。尽管AI在数学研究中的角色仍存在争议，但在形式化领域，AI的作用无疑是积极的——它有助于维护数学知识体系的严谨与可信。

原标题：Formalizing Fermat's Last Theorem。 HN 原始发布时间：2026年9月5日星期六。当前记录为 747 分、480 条评论。

阅读原文 · 查看 HN 讨论