登录
在一个密闭容器里做可逆反应，无论一开始怎么配比，最终是不是都会停到同一个平衡点？这个听着像“常识”的问题，1974 年由化学家 Fritz Horn 正式提出，此后半个世纪一直挂在化学反应网络理论的难题清单上。 2026 年 10 月下旬，把它“破解”冲上热搜的是 AI：一个 Claude Opus 5.5 指挥 136 个 GPT-6 Astra，用 11 天完成了这道猜想的证明，并公开了 83 个 Lean 形式化文件。 每一步推导都交给 Lean 4 内核检查，对就是对，错就是错。知乎专栏新智元
不过在转发热潮里，最要紧的一条事实几乎没人讲：这道“50 年难题”并不是一个人类证不出的未解之谜。早在 2015 年，数学家 Gheorghe Craciun 就在 arXiv 上公开了证明这一“全局吸引子猜想”的论文，此后论文多次修订，2026 年 9 月发布了进一步整理和扩展的版本。 而 AI 论文在“与已有工作的关系”一节里自己也承认，Craciun 的证明已经覆盖了它攻克的这一类情形，新路线的价值在于直接、只用初等工具，并且从持久性到收敛全程机器可检。 所以这条热搜里真正被“攻破”的，不是证不出的问题，而是 AI 端到端跑完一个自然科学长程证明任务、且全程可被机器核验这件事本身。ChemDraft知乎问答
这个被背了 50 年的结论，为什么难证
它有个正式的名字：全局吸引子猜想（GAC），核心问题是：在同一个化学计量兼容类中，所有正初始浓度出发的轨迹，是否最终都会收敛到该类唯一的正平衡点？ 用大白话说：只要各物质的总量关系不变，起点怎么配，终点都一样。ChemDraft
直觉上“显然成立”，严格证明却难了半个世纪。1972 年，Horn 和 Jackson 找到了武器：一个类似熵的量，反应进行时只降不升，系统像一颗沿山坡下滚的球，滚到谷底就是平衡；他们一度以为问题解决了，但山坡上藏着一个陷阱：某种物质的浓度可能一路贴向零，在那里坡几乎变平，看着像谷底，其实是个假终点。 把这半个世纪的硬骨头说白，就是证明“下坡路”不会在边界上停下。知乎专栏
AI 的 11 天：一个决策者、136 个执行者、不足 60 行人工核对
按项目方的披露，这套流程分三层：Claude Opus 5.5 负责定方向——走哪条路、换掉哪一步；136 个 GPT-6 Astra 负责写证明、写 Lean 代码、编译、读报错、再修；每一步形式化证明交给 Lean 内核裁决。转折出现在第 6 天：执行智能体陆续报回，教科书路径要补的地基太多、工程量太大，决策智能体没有让它们硬啃，直接换了一条路，第二天，卡住的那一步编译通过。
人类留在环节里的把关很薄：研究者定题目、核对机器检查的那个命题说的确实是这道题，要人核对的部分不到 60 行。不过边界也要划清：严格地说，论文证明的是这个猜想里满足细致平衡的一类情形，第一步借助了已有的定理；从那里到终点，整条证明链都过了机器检查。知乎专栏
那这条热搜还值不值得看
先看这项工作的“化学”浓度：它属于化学反应网络的数学模型，离实验台并不近。做这个方向的人本来就少，2015/2016 年的两版证明只完整写出三、四维的低维情形，一般 n 维的论证是 2026 年 9 月的 v3 才补全的，一个月后被 AI 发掘并重新证明。 换句话说，人类数学界一个月前刚把地基浇完，AI 挑了一条更短的路重走一遍，并全程装了“行车记录仪”。知乎问答
真正值得关注的变化在核验方式：过去，一份证明要几位专家逐行审上几个月；现在，它可以附带一份机器检查，过程也附带一份完整记录。 需要留个注脚：11 天、136 个智能体、云端工作站预装 533 个科研软件与工具等数字，全部出自项目方自己公布；ClawsGO Science 正式版已上线、实验室正在融资，目前还看不到外部学界的独立评审意见。知乎专栏
“AI 要斩杀理科生”？化学家们更关心下一个问题
热评里最响的情绪是危机感：AI 要来斩杀理科生了！ 但更专业的讨论把问题拉回尺度：这个猜想本质是化学的数学模型命题，被自动化的是“形式化推导”这一环，不是烧杯、通风橱和柱层析。ChemDraft
化学圈真正想要的那件“圣杯”是另一幅图景：你提一个合成思路或材料方向，AI 没日没夜地帮你完成路线修正、合成实验、材料标准、模拟计算、论文写作，全程不用碰危险试剂。 有人调侃，这种“AI 全自动机器人”在现实里的名字叫“博士后”。玩笑背后是真问题：从定理到实验，中间还隔着整个湿实验环节。知乎问答
还有一个读这条热搜的姿势问题：传播最广的两篇“解读”，一篇来自正在天使轮融资的实验室的官宣，一篇则把热点直接接进了自家产品的推广，它在文末写道，在研发 ChemDraft 的过程中，他们也一直在尝试把 AI 带进化学科研的日常工作中。 “攻克”叙事带着产品宣传的底色，接受这些信息时值得先打个折。ChemDraft
接下来值得盯的，不是下一个“AI 攻克 X”的标题，而是两件事：这份 Lean 证明会被反应网络理论的研究者接纳，还是被挑出毛病；这种“定题—形式化—机器核验”的流程，何时撞上真正没有现成答案可循的自然科学问题。那才是判断 AI 科研成色的时刻。
