Axiom AI 智能体集群用 24 天完成有限单群分类定理形式化验证
精选理由
一个 AI 智能体集群花 24 天验完了数学界 40 年没人能独立核查的最长证明，还揪出 34 处文献错误，太狠了。
Axiom 的 AI 智能体集群用 24 天把有限单群分类定理约 15000 页、覆盖 500 多篇论文的证明内容转化为超过 3800 万行机器可验证代码。数学界此前 40 多年无人能独立核查这一史上最长的证明。验证过程中还发现了已发表文献中的 34 处严重出入。
原文 · rohanpaul_ai
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.
