作者称 Verified AI 迎来标志性月份，Axiom 的 AI 智能体集群用 24 天完成数学史上最长证明的验证，将跨越 500 多篇论文的 15,000 页有限单群分类定理（CFSG）转化为 3800 万行以上机器验证代码，并发现已发表记录中的 34 处严重出入。引用内容补充称该形式化证明可能是最大的开源项目之一，图中显示 Axiom CFSG 达 43.0M 行，约每 37 天翻倍。
原文汇总了 AI 智能体集群形式化验证有限单群分类定理的规模数据，可作为观察形式化验证能力进展的一个参照点。
Verified AI 刚刚迎来了它最辉煌的一个月。
一群 AI 智能体刚刚完成了任何数学家都无法独自完成的事：检查了历史上最长证明的每一个步骤。
40 多年来，数学家们一直在有限单群分类的基础上继续研究，却没有人能够独自核验它。
Axiom 的 AI 智能体集群仅用 24 天就完成了这项工作，将 500 多篇论文中的 15,000 页内容转化为 3800 多万行机器验证代码。它还发现了已发表记录中的 34 处严重差异。
CFSG 的形式化证明如今可能已成为有史以来最大的开源项目之一。观看智能体将其组装起来，让人再次意识到其背后那令人敬畏的人类成就。这张图代表了数学家们数十年来发展出的约 15,000 页错综复杂的论证。
原文
The formal proof of CFSG may now be among the largest open-source projects ever. Watching agents assemble it is a reminder of the awe-inspiring human achievement behind it. The graph represents some 15,000 pages of intricate arguments developed by mathematicians over decades.
来源：Rohan Paul · x.com