10月22日，arXiv上出现一篇23页的论文，研究“细致平衡质量作用系统的全局收敛”。
报道要热闹得多：BitMiracle AI Lab的ClawsGO Science，让1个Claude Opus 5.5指挥136个GPT-6 Astra，用11天“破解”了1974年的化学猜想。新智元
热搜词条更短：“困扰化学界50年难题被AI攻破。”但论文第一节“与已有工作的关系”承认，Craciun的证明已经覆盖了这种情形。arXiv
这篇2015年的预印本，摘要写得更直接：所有细致平衡的质量作用系统，都具有全局吸引子性质。arXiv
论文对自己的定位很克制：路线更直接、只用初等工具，主定理从持久性到收敛都交给Lean内核检查。arXiv
先把题说清楚。1974年，化学家Fritz Horn提出“全局吸引子猜想”：密闭容器里的可逆反应，不管最初怎么配料，只要守恒量相同，最后是否一定停在同一个平衡点？
直觉上应该会。难的是排除边界：某种物质浓度可能一路趋近于零，熵的“山坡”在那里几乎变平，看起来像谷底，其实是假终点。
1972年，Horn和Jackson找到类似熵的量，反应过程中只降不升。此后半个世纪，研究者一直在补“边界不会吸走轨迹”这一步。
AI这次证的，是猜想里“细致平衡”的一类情形：每条正反应的速率等于其逆反应的速率。
报道也承认：第一步借助了已有的定理。新智元
证明分两段。有界性和持久性用了OpenAI在2026年论文里的定理；对应到Lean里，是71个模块、约7900行改编代码。arXiv
真正为新论文写的，是熵论证、平衡点唯一性和收敛部分，约1400行。其中一步用“有界速度下降”替代LaSalle不变原理，绕开了解唯一性和初值连续依赖。
所以，最准确的说法不是“AI证出了50年没人证出的题”，而是“AI在11天里，把一个已知可证的命题，做成了一条完整、可编译、可复查的证明链”。
这仍然值得认真看。数学论文里一句“显然”背后可能藏着漏洞；Lean内核不看作者是谁，只认每一步是否符合形式规则。
公开仓库里有84个 Lean 文件。审计脚本检查了35个声明，结果只落在三个标准公理上。GitHub
论文还写明：人类作者负责指导工作、核对论证以及Lean陈述与数学定义的对应，并对内容负全责；AI不算作者。arXiv
“不到60行”的说法要打个折扣。论文原话是：形式化陈述加上它依赖的定义，在Mathlib之上不到60行。人要确认的是“这段代码说的正是定理1.1”；证明本身有九千多行，大部分交给机器检查。arXiv
那这件事的分量在哪？不在“化学”，也不在“50年”。论文没有做实验，也不涉及具体分子；它解的是一个化学反应网络理论里的数学问题。
真正的变化在流程：AI把“写证明—形式化—编译—改错”跑成了闭环，而且这次跑得很快。
但它能跑通，前提是这道题有明确的形式化目标、有现成定理可借、还有一个能给出对错的内核。换个没有已知证明、连命题都还没说清的问题，这套流程能不能启动就难说了。
知乎答主“想象中”读完论文后判断更直接：这和之前炒作“AI攻克费马大定理”类似，是找到了初等的、不绕路的方法，并通过了机器检查。知乎
还有个细节：这篇论文的持久性部分，直接借用了OpenAI在2026年的一份形式化工作。一个AI实验室的证明，成为另一个智能体团队的起点。
这条链有多结实，要看接下来有没有独立研究者去读那九千行、去把一般情形搬进Lean、去把这套流程用到没有现成答案的问题上。
截至11月3日，论文还是arXiv预印本；公开仓库只有一次初始提交、5个star、1个fork、0个issue。热闹是热搜的，检验才刚开始。
