Axiom 智能体集群用 24 天形式化验证有限单群分类证明
Verified AI just had its greatest month.
Axiom 的 AI 智能体集群用 24 天完成了有限单群分类（CFSG）证明的逐步验证，将 500 多篇论文、约 15000 页内容转成 3800 万行以上机器可验证代码，并发现已发表记录中 34 处严重不一致。该证明此前 40 多年无人能独自完整核验。
查看原帖CFSG 的正式证明如今或许已成为有史以来规模最大的开源项目之一。观看智能体们将其组装起来，让人想起其背后那令人敬畏的人类成就。这张图代表了数学家们数十年来发展出的约 15000 页错综复杂的论证。https://t.co/13THDKI50f
查看原文
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. https://t.co/13THDKI50f
正文
Verified AI just had its greatest month.
A swarm of AI agents just did what no mathematician could do alone: check every step of the longest proof in history.
For 40+ years, mathematicians have built on the Classification of Finite Simple Groups without anyone being able to check it alone.
Axiom’s AI agent swarm just did it in 24 days, turned 15,000 pages across 500+ papers into 38M+ lines of machine-verified code. And it also uncovered 34 serious discrepancies in the published record.