**数学史上最长证明获计算机验证：Axiom 用 AI 完成有限单群分类定理的形式化**

_Formalizing the Enormous Theorem_

> Axiom 项目利用 AI 代理群在 Lean 证明助手上完成了有限单群分类定理（CFSG）的形式化，这是人类历史上篇幅最长的数学证明。该项目历时 24 天，生成了约 4310 万行代码，不仅验证了原证明中的 34 处偏差，还衍生出新的群论结果，并揭示了有限单群与量子物理及黑洞熵之间的深刻联系。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-models
- **发布时间**：2026-10-27 22:57（北京时间）
- **原文**：[打开原文](https://axiommath.ai/research/the-enormous-theorem-formalized)