Lean 4 完成费马大定理机器验证

Fermat's Last Theorem in Lean 4

Anthropic 在 GitHub 上开源了费马大定理在 Lean 4 中的完整机器验证证明。该项目基于 Mathlib，复现了 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles 的经典论证路径。证明过程经过 Lean 内核与独立 Rust 内核 nanoda 的双重校验，确保仅依赖三个标准公理，未使用任何 sorry 或额外假设。整个证明包含超过 6 万个模块，生成的静态网页允许用户离线浏览每一步推导。这是 AI 代理在人类开源代码基础上构建、以 Lean 为仲裁者完成的里程碑式成果。