一句话看懂：Anthropic 在 GitHub 上开源了费马大定理的 Lean 4 完整机器检查证明，该证明已通过 Lean 内核、独立 Rust 内核及对比器的三重验证，成为 AI 与形式化数学交叉领域的重要工程里程碑。
事件核心：发生了什么
Anthropic 于近期发布了名为 “Fermat’s Last Theorem in Lean 4” 的研究工件，这是一个完全由机器检查的费马大定理证明仓库。该证明建立在 Lean 4.33.1 和 Mathlib v4.33.0 之上，论证路径沿用了 Frey、Serre、Ribet、Wiles 及 Taylor-Wiles 的经典思路。项目包含 60,475 个模块，共 29,511 个定理，耗时 5 小时 32 分钟完成构建（96 个并行任务，峰值内存 153 GB）。项目声明最终定理只依赖 Lean 的 propext、Classical.choice、Quot.sound 三个标准公理，不含 sorry、axiom 等未完成项。
为什么重要
这项工作的重要性在于验证链条的完整性与独立性。除 Lean 官方内核外，Anthropic 还使用了独立用 Rust 编写的 Lean 内核 nanoda 0.4.13 检查了 1,052,234 个声明，全部通过且无错误。此外，通过 leanprover/comparator 工具对比确认，证明中使用的所有定义与库存 Mathlib 完全一致，排除了“自定义公理”或“偷换命题”的可能。这意味着从工程层面看，费马大定理的证明已经可以在不信任任何特定证明助手的条件下，被两台独立实现的机器内核完整复验。这是对定理证明可靠性的极大增强，也展示了工具链的成熟度。
对用户/开发者/创作者的影响
对于形式化数学研究者和 Lean 开发者，这是一份高质量、可直接离线阅读的参考材料；项目自带约 390 MB 的静态 HTML 页面，提供了逐步证明路径、依赖图及全文搜索，大幅降低了理解门槛。对于 AI 从业者，这个案例展示了当前大模型推理能力与交互式定理证明结合的实际产出，尽管项目本身是“研究工件”且明确不接受贡献，但其验证规范（如依赖列表、公理审计）为后续 AI 生成证明的可靠性评估树立了范本。对普通开发者而言，5 GB 内存/并行任务和 220 GB 临时文件的构建需求提醒：这类验证任务的算力门槛依然相当高。
AI 工具推荐
想把多个 AI 模型放在一个入口？
GamsGo AI 集成 ChatGPT、DeepSeek、Gemini、Claude、Midjourney、Veo 等常用模型，适合写作、绘图、视频和日常 AI 工作流。
推广链接：通过此链接购买，我可能获得佣金，不影响你的价格。
值得关注的后续
目前公开信息显示，Anthropic 未表态是否会将该验证流程产品化。值得观察的点有三个：其一，这个仓库是否会被 Mathlib 社区吸收为常驻内容，还是停留在一次性研究层面；其二，nanoda 内核的几项性能补丁（仅提升判定效率、未改动类型规则）是否会被上游接纳，从而让独立内核的日常使用更可行；其三，Anthropic 是否会发布配套技术报告，说明该证明在 AI 辅助搜索或证明项生成中投入了多少模型推断资源，这将直接反映当前大模型在长链条数学推理上的真实成本。
