Anthropic 完成 1300 万行 Lean 费马大定理机器验证证明
davidad · x · 2026-09-05
Anthropic 宣布完成费马大定理的首个端到端、机器可检验的 Lean 证明，共 1300 万行 Lean 代码、包含 29500 个中间定理，被称为“有史以来构造的最大 Lean 证明”。
- 证明代码已公开，Kevin Buzzard 撰写了相关博客解读
- 社区随后讨论：能否像“速通”一样，用更少字符的 Lean 证明定理，作为新的竞技形式
所属事件:Claude 11 天形式化费马大定理，1300 万行 Lean 创纪录(31 条相关)→
「漫话AGI」频道最新
- Freeman Dyson 回忆 Bethe 解题法:面对难题先动手算,别被劝退 — CatAstro_Piyush · 2026-09-05
- 哲学家 Benjamin Bratton：常收到 AI 智能体来信请教如何构建 AI 社会 — bratton · 2026-09-05
- Thought Communication 论文：让模型用隐状态直接「读心」协作 — burny_tech · 2026-09-05
- 博主断言：模型正取代 UI 成为人机交互界面，语音是入口 — manosaie · 2026-09-05
- 最后的护城河:你能多快把原型造出来,仅此而已 — _Stocko_ · 2026-09-05
- 互动时间线复盘 Yudkowsky 三十年 AI 预测：准确度惨淡 — Chris_Armstrong · 2026-09-05