RecodeX 重构消息，AI数学公司Axiom宣布，其AI智能体在Lean证明助手中完成了有限单群分类定理（CFSG）的完整形式化验证。该定理原始证明超过1.5万页、分散于数百篇文献，此前能完整读懂全部论证的学者已日渐稀少。

团队依托现有数学库及此前积累的群论代码，将整套论证拆分后调度数十个AI智能体协同工作，历时24天写出约4310万行Lean代码并开源。过程中还排查出大量文献笔误、数据错误与遗漏前提，并在关键论证处发现原公开证明的疏漏，联合资深数学家补全了替代论证路线。