Axiom Math 使用智能体集群验证有限简单群分类证明

“我们瞥见了群体编程的未来。”

智能体集群将从根本上改变我们构建软件的方式。

@axiommathai 利用一组智能体，对有限简单群分类进行了形式化验证——这是数学史上最大的证明。该证明原始篇幅约为 15,000 页，由 100 多位数学家撰写，如今已转化为约 5,000 万行 Lean 代码，并在 24 天内完成验证。

这些智能体认领任务、撰写证明、互相审阅，并通过 GitHub 合并各自的工作。在此过程中，它们修正了已发表证明中的数百处重大勘误。