agent 集群 24 天形式化 15000 页有限单群分类，瓶颈在验证不在生成
docdavkitty · reddit · 2026-10-28
Axiom 于 10 月 26 日发布有限单群分类定理（CFSG）的完整 Lean 形式化：4310 万行代码、205 万个声明，耗时 24 天，由数十个 agent 组成的集群通过 GitHub issues 和 Slack 协调，拆分为 108 个里程碑完成（其中约 120 万行继承自早期项目）。
更值得注意的是失败日志：
- agent 需要引理时可以自己证明或直接假设，而在几十个 agent 的集群里，「假设」永远是最便宜的选择——导致数万行代码被删、部分计划重启；判断「给定理加一个假设是推迟了工作还是改变了含义」是反复出现的难题。
- 第二个瓶颈是 Lean 校验证明的速度跟不上 agent 的产出速度，团队用分布式缓存和可外部校验的证书（certificates）解决。
作者的核心结论：两个瓶颈都是验证端的吞吐限制而非生成端。任何要把 agent 接进正确性关键场景的人，撞到的天花板都会是验证。
所属事件:Axiom 用 AI 集群 24 天完成史上最大数学证明的 Lean 形式化(32 条相关)→
「编程与Agent」频道最新
- 一年级娃和爸爸用 Claude 一起做数学游戏,刷题刷疯了 — neuroecology · 2026-10-29
- 男子用 Claude Code 加备用安卓机自动刷 Hinge,日配 20-25 个 — pritisinghhhh · 2026-10-29
- 开发者：OpenAI Dot 加 24/7 Mac Mini 让生活改善 15% — willdepue · 2026-10-29
- 让 Agent 合入生产代码前,先装好这三道护栏 — Arindam_1729 · 2026-10-29
- EverOS Cloud 实测：让 Claude 新会话记住店铺退换规则并补出漏洞 — Aiden_Tech_Ai · 2026-10-29
- 量化交易 Python 新库 Ziplime 发布:用 AI 自然语言生成策略并回测 — mdancho84 · 2026-10-29