先把标题里的数字拆掉：这次不是 136 个不同的大模型坐在一起开会。按项目方的说法，是 1 个 Claude Opus 5.5 做决策，136 个 GPT-6 Astra 智能体执行，前后 11 天。 4 位人类作者负责指导、核对，并对内容负最终责任。136 个智能体背后是同一个模型——它们不是 136 票，而是 136 双手。微博
这套配置产出的，是 BitMiracle AI Lab 在 10 月 22 日挂上 arXiv 的一篇预印本。GAC 问的是：一个可逆反应网络，从不同的初始浓度出发，最后是否都会收敛到同一个平衡点。论文针对细致平衡情形给出了一条新的证明路线，并把整条链写成 Lean 4。
论文里写明的分工是：Opus 决定研究路线，Astra 写证明和 Lean 代码、跑编译、改错误，Lean 内核逐段检查。 人类作者则核对论文与形式化陈述的对应关系，并对内容负责。arXiv
幻觉是怎么被挡住的？不是靠 136 个模型互相投票，而是靠一个不看语气的裁判。Lean 是一个证明检查器：把数学证明写成代码，它按逻辑规则一步步验算。Astra 每写一步形式证明，就直接送进 Lean 内核；内核只认类型检查，不认“这步显然成立”。
全量编译之外，团队还做公理审计：主定理和主要中间结果只依赖 propext、Classical.choice、Quot.sound 这三条标准公理。 代码里没有 sorry、admit，也没有额外公理或 native_decide。模型可以一本正经地胡说，但它胡说的那一步过不了编译器。GitHub
但 Lean 只能保证“从形式化前提到形式化结论”的推导没错，它不知道你形式化的到底是不是原来那个定理。论文把这件事说得很直白：主定理的陈述和它依赖的定义，在 Mathlib 之上不到 60 行；这 60 行是不是准确表达了论文里的 Theorem 1.1，需要人来核对。 机器的活是把几千步推导压成“通过/不通过”，人的活是守住那个翻译层。这次人类作者的工作，主要就落在这里。arXiv
所以，把这件事说成“AI 独立解决了 50 年悬案”，并不准确。GAC 早在 2015 年就由 Gheorghe Craciun 给出了证明。他的摘要里写得很清楚：所有细致平衡的质量作用系统，都具备全局吸引子性质。 这次论文的引言也承认，Craciun 的证明覆盖了这类情形。它真正的贡献是：一条更初等、更直接的新路线，以及从持久性到收敛的整条链的机器验证。arXiv
论文里还有一个数字：约 9,300 行 Lean 代码，其中约 7,900 行是从 OpenAI 今年 9 月那份弱可逆系统持久性形式化里改编来的，剩下约 1,400 行才是为这篇论文新写的。它站在另一份形式化成果上。这个领域的进展，已经不是单点突破，而是开始互相搭脚手架。
项目方还披露了一个过程细节：第 6 天，几十个执行智能体陆续报回同一个问题——教科书上的路线要补的地基太多，工程量快撑不住了。Opus 5.5 没有让它们硬卷，而是换了路线；第二天，卡住的那一步编译通过，后来成了论文里的关键一步。这个细节比“136 个模型”更能说明多智能体在做什么：不是投票，是并行试错和及时止损。
论文也没有把话说满：Wegscheider 判据、数值例子，以及复平衡系统的扩展等部分没有形式化。 这篇论文还是预印本，三组并行复核由智能体运行框架（harness）完成，不等同于外部同行评审。arXiv
这次最值得看的地方，可能不是 136，也不是 11 天。AI 做科研的瓶颈，一直不只是“会不会想”，还有“错了谁来发现”。在数学这种有 Lean 的地方，错误可以被编译器挡住，检查的重心从“几位专家逐行审几个月”，变成“跑一次构建，再守住那几十行陈述”；在化学、生物、材料这些没有统一证明检查器的领域，AI 仍然要面对实验、数据和可复现性的慢验证。ClawsGO 这类平台把科研软件和数据库搬进云端，软件可以预装，但湿实验不会因为软件预装而自动变快。
136 个智能体、11 天、9,300 行，这些数字都很好记。真正决定这篇论文能不能信的，是那不到 60 行——人类还要读、还要确认“我们证的是不是我们想证的那个东西”。AI 把证明变便宜了，但没有把“证明什么”变便宜。
