Axiom 用 Lean 完整形式化有限单群分类定理，史上最大数学证明获机器验证
GuillaumeLample · x · 2026-10-28
Axiom 宣布完成对有限单群分类定理（Finite Simple Groups Classification，对称性的「元素周期表」）的完整 Lean 自动形式化，称这是人类史上最大的数学证明获得计算机验证。
该定理原始证明约 15000 页，由 100 多位数学家跨越数代人合作完成。Meta 的 fcharton（Guillaume Lample 转发）评价：这是「现实数量的人类数学家在合理时间内不可能完成的有用数学」，是不同于常见的「最后一公里抢发」的真正进步。
所属事件:Axiom 用 AI 智能体 24 天 Lean 形式化有限单群分类定理(34 条相关)→
「研究」频道最新
- kalomaze:比 Transformer 更好的架构一直有,只是被当作「魔改 Transformer」 — cephaloform · 2026-11-03
- 开源 NorthCUA 电脑操作模型发布，Pro 版多项基准超中国大厂旗舰 — Powerful_Evening5495 · 2026-11-03
- 宇树 G1 学会自我脱困，ROOF 强化学习策略无需视觉地图 — Scobleizer · 2026-11-03
- ACM 期刊全面转双盲说法被澄清：TOSEM 暂仍单盲 — mboehme_ · 2026-11-03
- DeepMind 992人RCT：亲密感上升主因是重复使用而非个性化 — Dr_Atoosa · 2026-11-03
- Weight-Space Programming 直接编辑 Qwen 模型，模型与 Demo 已开源 — kalyan_kpl · 2026-11-03