Axiom 宣布人类史上最大数学证明完成 Lean 机器验证
TheTuringPost · x · 2026-10-28
Axiom 宣布完成有限单群分类定理（The Classification of Finite Simple Groups，「对称性的元素周期表」）的完整 Lean 自动形式化，称这是人类历史上最大的数学证明首次被计算机完整验证。
- 规模：约 15,000 页，由 100 多位数学家跨数代人积累而成
- 方法：动用大量 AI agent 进行自动形式化
- 关键价值：过程中还修复了原证明中历史上的缺口
这一工作被视为 AI 形式化数学的标志性成果。
所属事件:有限单群分类定理完成 Lean 形式化，史上最大证明获机器验证(21 条相关)→
「漫话AGI」频道最新
- 借 Claude Code 跳过权限flag喻人生：你的bodymind正开着autopilot — mimi10v3 · 2026-10-28
- Ethan Mollick："AI 全是假的"阴谋论已被证据驳倒，但仍会继续误导公众 — emollick · 2026-10-28
- Whop CEO：月近 10 万人变现，agent 流量已超过真人用户 — LexSokolin · 2026-10-28
- OpenAI 最新数据：ChatGPT 消息近半数是 Google 式搜索提问 — VeryWellVersed · 2026-10-28
- 决策理论辩题：能否可预测地对比你笨的 Omega 选择 one-box — jessi_cata · 2026-10-28
- 研究者：AI 解放了发表或出局的苦役，重拾大胆想法 — DrCirillo · 2026-10-28