RecodeX 重构消息，数学界一项重大成果：有限单群分类（Classification of Finite Simple Groups）已在Lean证明助手中完成形式化。该分类是群论领域规模最大、结构最复杂的定理之一，其完整证明分散于数万页文献之中。此次形式化意味着这一结论可被机器逐行验证。