**有限单群分类定理在 Lean 中完成形式化验证**

_Classification of Finite Simple Groups Formalized in Lean_

> 首个有限单群分类定理的完整证明已在 Lean 中实现形式化，且每一步逻辑均通过内核验证。在此过程中，研究人员发现了现有“不平衡群定理”证明路线中的反例，并基于所罗门 1976 年的理论提出了替代论证方案。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-models
- **发布时间**：2026-10-28 00:29（北京时间）
- **原文**：[打开原文](https://cfsg.axiommath.ai/)