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 为仲裁者完成的里程碑式成果。
没有任何工具能检查每个中间定理是否如其名称所暗示的那样，这需要读者自行判断。
HN 评论区
32- black_knight
我想知道 Lean 代码中是否有任何部分可以整理成适合贡献给现有 Lean 库的形式。
根据我的经验，要让 Fable 写出足够好、能被他人用于形式化库的代码，需要大量的人工干预。但既然这里肯定也形式化了很多前置条件，如果这些努力没有全部浪费在某个终极证明上，那就太好了！
（这是之前评论的重发，但我觉得放在这里更合适）
- superposeur
证明的价值很大程度上在于为了达成目标而发展出的数学定义和中间定理，就像 Grothendieck 风格那样。这种能力似乎仍然超出了 AI 的范畴（至少，我还没听说在最新一波 AI 证明中涌现出像“概形”或“模形式”这样根本性的、有用的新定义）。不过，我在想 AI 是否也能通过某种过程掌握这项技能：高效地将一个庞大的 Lean 证明重构为 Lean 代码片段，然后将这些片段重新解释为具有生动名称的、人类可理解的新定义？
- mcapodici
活在这个时代真是令人激动。
https://github.com/anthropics/fermats-last-theorem/blob/main...
- chvid
我觉得一个有趣的问题，甚至可能更有趣的问题是：最短、最简洁、最容易理解（且可形式化验证）的证明是什么。
- rawling