史上最长数学证明被机器验证：Axiom 用 Lean 形式化 1.5 万页有限单群分类

IgorCarron · x · 2026-10-28

Axiom 宣布完成人类历史上最长数学证明的计算机验证：有限单群分类定理（被称为「对称性的元素周期表」）的完整 Lean 自动形式化。该证明约 15,000 页，由超过 100 位数学家历经数代人协作完成，此前远超单人能阅读理解的规模。

转发者 BlancheMinerva 评价称，对人类无法完整阅读的长证明做形式验证是件大事。她还披露：Axiom 几天前发邮件请她推广，通常她会拒绝这类请求，但这次的内容即使不请她也会主动转发。