AI 用 24 天让计算机核对完数学史上最长的证明
Axiom 数学公司用几十个 AI agent 花费 24 天，将约 1.5 万页、500 多篇论文构成的"有限单群分类定理"（巨大定理）证明完整改写为 Lean 可检查代码并全部通过核查。定理结论成立，但发现 John Walter 1986 年关于"不平衡群定理"的证明存在漏洞，AI 借助 Solomon 1976 年思路写出新证法并通过检查。项目共产出约 4310 万行代码，AI 与人类数学家分工协作。Lean 可保证每步推导正确，但定理陈述的翻译准确性仍需人工核查，目前尚无外部独立验证。
