可验证 AI 的重大胜利。

形式化数学证明正开始像软件一样规模化扩展。

@axiommathai 重写了数学史上最长的证明，整整 15,000 页，大约 4000 万行 Lean 代码。
在数学家的指导下，一群 AI 代理在 24 天内完成了编写。

Axiom 表示，今年年初时，让 AxiomProver 编写一个正确的 1,0000 行 Lean 证明还需要数周的调教。而现在，这群代理在 24 天内将一个大约是其 4000 倍规模的问题进行了形式化。

目标是有限简单群分类定理：大约 15,000 页、500 多篇论文、约 100 位作者，且没有哪位单一读者能完整读完所有内容。

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