数学史上最长的证明之一——有限单群分类定理（CFSG）——近日完成机器验证。据作者披露，Axiom的AI智能体集群在24天内完成了这一工作，将原本横跨500多篇论文、约15000页的证明内容转化为机器可检验的形式化代码。

验证产出的代码规模超过3800万行。相关图示显示，Axiom CFSG已达到43.0M行，并呈现约每37天翻倍的增长节奏。引用内容指出，这一形式化证明可能是规模最大的开源项目之一。

除完成验证外，该过程还发现已发表记录中存在34处严重出入。这些差异的具体性质及其对原始证明的影响，原文未作进一步说明。

作者将这一进展称为Verified AI的标志性月份。对AI行业而言，此次案例展示了智能体集群在超大规模形式化任务中的协作能力，也为数学文献的机器校验提供了可参照的工程样本。