Axiom 用 AI 智能体集群重写有限简单群分类的 15,000 页形式化证明

AI 导读

Axiom 称，AI 智能体集群在数学家引导下用 24 天完成了有限简单群分类约 15,000 页、约 4,000 万行 Lean 的形式化证明。此前写出正确的 10,000 行 Lean 证明还需数周引导，此次规模约扩大 4,000 倍。Axiom 将这一变化归因于同时重建模型、harness 与基础设施三层。

正文 · AI 翻译

可验证 AI 领域的一次重大胜利。

形式化数学证明开始像软件一样实现规模化。

@axiommathai 重写了数学界最长的证明——足足 15,000 页、约 4,000 万行 Lean 代码。

一群 AI 智能体在 24 天内完成了编写，数学家则负责引导它们。

Axiom 表示，就在今年年初，让 AxiomProver 写出一份正确的 1 万行 Lean 证明还需要数周的反复引导。而如今，这群智能体在 24 天内形式化了一个规模约为前者 4,000 倍的问题。

目标是《有限简单群分类》：约 15,000 页、500 多篇论文、约 100 位作者，而且没有任何一位读者通读过全部内容。

Axiom 将这一跃升归功于同时重建了三个层面：模型、测试框架和基础设施。