Axiom 完成有限单群分类定理的完整 Lean 形式化，约 1.5 万页证明获机器验证

Axiom 宣布完成有限单群分类定理的完整 Lean 自动形式化，约 15,000 页的证明由此获得计算机逐行验证。该定理由 100 多位数学家跨越数代人积累而成，此前因篇幅过大无法被整体机器校验。此次形式化被视为 AI 辅助形式化数学的标志性成果。