文章总结： Anthropic的ClaudeAI在11天内完成费马大定理的机器可验证形式化证明，生成1300万行Lean代码、29511个定理，由KevinBuzzard确认正确性。项目使用Prove2Me平台并行处理，消耗60亿输出tokens，构建需230GB内存。这是将已有证明形式化而非发现新证明，资源门槛高且平台未开源。 综合评分： 78 文章分类： AI安全,解决方案,其他

Anthropic Fermat’s Last Theorem形式化项目：AI在11天内完成数学里程碑证明（1300万行L…

原创

AI Online AI Online

人工智能online

2026年9月13日 08:27 日本

在小说阅读器读本章

去阅读

在公众号小说中沉浸阅读

Fermat’s Last Theorem困扰数学家358年，Andrew Wiles 1995年的129页证明曾耗费数月人工验证，而Claude仅用11天便完成了等价的机器可验证形式化[2]。本篇旨在帮助读者判断：该项目完成了什么、关键数字的实际含义、资源门槛，以及AI形式化能力的边界。

本文基于2026年9月12日前公开可获取的信息撰写，评估截止日期为2026-09-12。

项目定位与声明

NOTE

Apache-2.0开源许可，GitHub公开，Kevin Buzzard确认正确性

项目名：anthropics/fermats-last-theorem 核心价值：将Wiles的Fermat’s Last Theorem证明完整形式化为Lean 4证明助手可验证的代码，证明本身不依赖任何额外公理或未验证假设[3]。 开源性质：Apache-2.0许可证，代码已在GitHub公开（Stars: 1129, Forks: 95）[1][3]。 版本：使用Lean toolchain 4.33.1 + Mathlib v4.33.0[3]。 可运行程度：代码可从GitHub克隆，构建需约5.5小时、峰值230GB内存[3]。 评估说明：README正文内容在证据中未完整呈现，部分技术细节（如Prove2Me平台架构、Claude具体协作流程）未公开。

项目由Anthropic研究员Tianyi Peng团队发起，旨在测试Claude在形式化数学证明方面的能力[2]。这并非AI”发现”了新证明，而是将已有人类数学成果转化为机器可验证形式——这一区分对评估AI数学能力边界至关重要[4]。

场景与痛点

形式化验证的瓶颈：Bergstra于2000年代中期提出形式化Wiles证明的想法，此后数学界持续开发必要工具，但预计需数年才能完成[2]。Kevin Buzzard于2024年在Imperial College London发起社区协作项目推进此工作[2]。 人力成本：Wiles原始证明129页，数学家花费数月逐行验证[2]。 社区协作局限：传统形式化依赖人类数学家逐条构建引理、填补细节，并行度受限于人力组织成本。

Tianyi Peng团队的突破在于：将形式化任务通过Prove2Me平台分解为小语句，分配给并行代理处理，Claude生成60亿输出tokens，实现11天完成而非数年[3]。这意味着单个研究团队可在合理时间内完成此前需整个社区协作的数学形式化工作。

核心功能

功能一：端到端形式化证明

机制：将Wiles 1995年证明的全部129页数学推理逐条转化为Lean 4的定理证明语句，涵盖数论、代数几何、模形式等领域的完整证明链条[2]。 可验证证据：项目产出29,511个定理、60,475个模块、13,000,000行Lean代码；构建耗时5.5小时（96并行任务）、峰值内存230GB、导出大小37.8GB[3]。Kevin Buzzard确认了结果的正确性[2]。 使用场景：假设研究者希望验证某条新数学定理的正确性，可参考此项目的目录结构与引理依赖关系，建立类似的形式化工作流。 关键约束：无sorry占位符——所有定理均已完整证明；仅依赖Lean内置的3个公钥（propext、Classical.choice、Quot.sound），未引入额外假设[3]。

功能二：大规模并行形式化工作流

机制：Prove2Me平台将完整证明分解为可独立处理的小语句片段，并行分配给多个Claude代理实例[3]。 可验证局限：Prove2Me具体架构、任务分配策略、代理协调机制未公开；Claude在形式化过程中的具体策略（是否有人工干预、错误修正流程）未披露[3]。 使用场景：假设形式化团队需在deadline前完成大型定理库，可采用类似分解-并行-合并策略，将完整证明拆解为若干独立子目标。 关键洞察：6 billion output tokens的输出量表明，Claude在此过程中进行了大量推理尝试与修正，而非简单线性生成。

功能三：零信任假设的形式化验证

机制：所有引理仅依赖Lean核心语言内置的3条公理，不依赖外部证明库的自定义公理或未验证假设[3]。 可验证证据：README明确声明无sorry占位符，形式化证明从数学基础到最终定理全程可机器验证。 使用场景：若研究者需将形式化证明作为信任锚点（用于元数学研究或形式化验证流程），此项目的无额外公理约束特性提供了可信基础。 局限：技术细节未公开，无法评估实际构建过程中的错误率或修正成本。

上手方式

证据中未提供完整的可运行示例或API调用方式，README正文内容未在证据中完整呈现。以下为可操作的替代路径：

TIP

构建需230GB内存、5.5小时，考虑使用云端或专业硬件环境

官方入口：GitHub仓库 来源] 工具链要求：Lean 4.33.1 + Mathlib v4.33.0[3] 预期构建流程（示意，以官方为准）：克隆仓库后配置Lean 4.33.1环境，执行lakefile.toml中定义的构建任务，构建过程约需5.5小时（96并行任务）、峰值内存230GB[3]。

建议关注：

• README中的形式化定理声明（对于正整数a, b, c和n≥3，a^n + b^n ≠ c^n）[3]

• 目录结构与模块依赖关系

• Kevin Buzzard的确认声明内容[2]

亮点对比

| 维度 | anthropics/fermats-last-theorem | Kevin Buzzard 2024社区项目 | leanprover/comparator | | — | — | — | — | | 规模 | 29,511定理、13M行代码 | 进行中，未公开完整数字 | 工具性质，非具体证明 | | 时间 | 11天（Claude） | 数月（社区协作） | N/A | | 资源 | 230GB内存 | 人力为主 | 轻量工具 | | 验证 | Kevin Buzzard确认 | 社区peer review | Lean CI自动验证 |

能力边界对比：anthropics项目在11天内完成了此前预计需数年的工作，但这是将已有Wiles证明形式化，而非创造新证明[4]。Kevin Buzzard的社区项目更注重引理的通用性与可复用性，而Claude驱动的形式化更追求完成速度。leanprover/comparator是轻量级工具，不具备完整形式化工作流能力。

选择建议：若需在学术论文中引用形式化证明作为信任锚点，选择有专家确认的anthropics项目结果；若研究目标涉及开发新的形式化工具链，关注Kevin Buzzard社区项目的引理积累；若仅需验证特定引理的Lean表述，leanprover/comparator类工具更轻量。

成熟度与风险

量化指标：Stars 1129, Forks 95, 最近提交2026-09-04, 最近更新2026-09-12[1]。 社区响应：7个open issues（截至评估日）[1]。

WARNING

本项目不适用于：计算资源受限环境、需要人工可读解释的场景、非Lean生态项目、需要实时协作的功能

不适用场景：

• 计算资源受限环境：230GB峰值内存、5.5小时构建时间的要求排除了普通开发设备[3]

• 需要人工可读解释的场景：Claude推理过程未公开，无法追溯具体证明策略

• 非Lean生态项目：项目基于Lean 4形式化，其他证明助手（如Coq、Isabelle）用户无法直接复用

• 需要实时协作的功能：Prove2Me平台机制未开源，其他团队无法复用此并行化框架

关键局限：README完整内容未在证据中呈现，无法评估文档完整性；Prove2Me平台架构未公开，其他团队难以复制其工作流；Kevin Buzzard确认的具体范围和深度未知。读者可核查GitHub仓库的issues响应速度、README完成度以评估维护状态。

快速决策与总结

决策树：

1. 你的需求是否需要形式化Fermat’s Last Theorem证明？

是 → 直接使用仓库代码，关注构建说明      否 → 进入下一步

2. 你是否需要了解AI形式化大规模数学证明的能力边界？

是 → 参考项目数字（11天、60亿tokens、零sorry），注意区分”形式化”与”发现新证明”[4]      否 → 进入下一步

3. 你是否有≥230GB内存的硬件环境？

是 → 可尝试本地构建，关注仓库issues了解已知问题      否 → 关注仓库后续优化或云端构建方案

IMPORTANT

本项目是AI形式化数学证明的里程碑事件，而非AI”发现”了新证明

总结：本项目是AI形式化数学证明的里程碑事件，11天内完成29,511个定理的形式化、仅依赖3个Lean内置公钥、Kevin Buzzard确认正确性[2][3]。资源门槛高（230GB内存）、Prove2Me平台未开源、具体协作流程未公开。推荐使用场景：学术引用、形式化方法研究、AI辅助数学工作流参考；谨慎尝试场景：需本地复现或修改；不推荐场景：依赖轻量工具或无法满足硬件条件。

关注指标：GitHub issues响应速度、README后续更新内容、是否有人提交基于此项目的下游工作。

参考来源

[1] GitHub – anthropics/fermats-last-theorem

[2] Formalizing Fermat’s Last Theorem | Anthropic

[3] Anthropic’s AI formalizes Fermat’s Last Theorem in Lean – DEV Community

[4] Anthropic Claude Formalized Fermat’s Last Theorem. It Did Not Discover the Proof | Remio

免责声明：

本文所载程序、技术方法仅面向合法合规的安全研究与教学场景，旨在提升网络安全防护能力，具有明确的技术研究属性。

任何单位或个人未经授权，将本文内容用于攻击、破坏等非法用途的，由此引发的全部法律责任、民事赔偿及连带责任，均由行为人独立承担，本站不承担任何连带责任。

本站内容均为技术交流与知识分享目的发布，若存在版权侵权或其他异议，请通过邮件联系处理，具体联系方式可点击页面上方的联系我。

本文转载自：人工智能online AI Online AI Online《Anthropic Fermat’s Last Theorem形式化项目：AI在11天内完成数学里程碑证明（1300万行L…》