omarsar0· @omarsar0 · X·· 4 小时前AI 评分
Axiom Math 使用智能体集群验证有限简单群分类证明
Axiom Math 使用智能体集群正式验证了有限简单群分类证明，这项工作约含 15000 页内容、由 100 多位数学家参与，现已转化为约 5000 万行 Lean 代码，并在 24 天内完成验证。智能体通过 GitHub 认领任务、撰写证明、相互审查并合并工作，同时修正了已发表证明中的数百处重要勘误。
"We saw a glimpse of the future of swarm coding."
Agent swarms will fundamentally change how we build software.
@axiommathai used a swarm of agents to formally verify the Classification of Finite Simple Groups, the largest proof in math history. That is roughly 15,000 pages by over 100 mathematicians, now about 50 million lines of Lean, verified in 24 days.
The agents claimed tasks, wrote proofs, reviewed each other, and merged their own work through GitHub. Along the way, they fixed hundreds of major errata in the published proof.
来源：omarsar0 · x.com