一个智能体集群在24天内完成了15,000页有限单群分类的形式化——瓶颈在检查器，而非模型
智能体集群24天完成有限单群分类Lean形式化
原文：An agent swarm formalized the 15,000-page classification of finite simple groups in 24 days — the bottleneck was the checker, not the models
Axiom于10月26日发布了有限单群分类的完整Lean形式化：4310万行代码、205万条声明、耗时24天，数十个智能体组成的集群通过GitHub issues和Slack频道协调，拆分为108个里程碑。其中约120万行继承自早前的项目。最值得读的部分是失败日志。需要某个引理的智能体可以选择证明它或假设它，而在数十个智能体组成的集群中，最省事的做法永远是直接假设。数万行代码不得不被删除，部分计划重新启动。第一个里程碑在前十二天内才完成。Axiom自己的说法是：判断给定理添加一个假设是推迟了工作还是改变了其含义，是一个反复出现的难题。第二个瓶颈是Lean重新检查证明的速度慢于智能体生成证明的速度，通过分布式缓存和可外部检查的证书解决了这一问题。两者都是验证环节的吞吐量限制，而非生成环节的限制。如果你正在将智能体接入任何对正确性有要求的场景，这就是你会撞到的天花板。
🖼 相关图片
