RecodeX 重构消息，数十个AI Agent仅用24天，完成了有限单群分类定理的Lean形式化。该定理此前由上百位数学家历经数十年、分散在500多篇论文中完成。此次形式化生成约4310万行可逐步验证的代码和205万个形式化声明，产出首份覆盖整个分类定理的计算机检查证明。

形式化过程中，AI排查出34处文献偏差，发现该定理相关研究中存在近40年的论证漏洞，并参与构造了新的群论结果。成果完全依托标准公理，无未完成证明的占位符，已全部公开。