Anthropic 完成 1300 万行 Lean 费马大定理机器验证证明
davidad · x · 2026-09-05
Anthropic 宣布完成费马大定理的首个端到端、机器可检验的 Lean 证明，共 1300 万行 Lean 代码、包含 29500 个中间定理，被称为“有史以来构造的最大 Lean 证明”。
- 证明代码已公开，Kevin Buzzard 撰写了相关博客解读
- 社区随后讨论：能否像“速通”一样，用更少字符的 Lean 证明定理，作为新的竞技形式
所属事件:Claude 11 天完成费马大定理首个形式化证明(52 条相关)→
「漫话AGI」频道最新
- Polymarket:OpenAI 年内全面暂停训练的概率仅 7% — Polymarket · 2026-10-21
- Daniel Lemire：AI 量产论文正在戳穿学术界的「教授庞氏骗局」 — lemire · 2026-10-21
- 学者吐槽:大学封杀爬虫下载论文,终身阅读量不足答辩委员会人数 — generativist · 2026-10-21
- 伯克利获 Schmidt Sciences 资助：用 AI 破解抹香鲸与虎鲸语言 — begusgasper · 2026-10-21
- 3Blue1Brown:即使 LLM 能做清晰讲解,我也会继续做视频 — 3blue1brown · 2026-10-21
- Talos 安全研究员:AI agent 攻击尚是吵闹渗透,蜂群静默红队才是真风险 — matthew_d_green · 2026-10-21