中学化学里有一句话：可逆反应最终会达到平衡。我们用它算平衡常数、算转化率。但很少人追问：这句话凭什么对所有起点都成立？
把 A 和 B 放进密闭容器，A ⇌ B。课本说，达到平衡时正逆反应速率相等，浓度不再变化；平衡常数只跟温度有关，剩下的由守恒量决定。于是有了一个说法：只要初始的守恒总量一样，最后总会停在同一个平衡点。1974年，化学家 Fritz Horn 把它写成了一个猜想。
这是一个关于微分方程全局行为的断言：从任意正初值出发，每一条轨迹是否都收敛到同一个正平衡点？会不会一直振荡？会不会某种物质先被耗光，贴到边界上，看起来不动了，其实停在一个假终点？对一般的反应网络，答案不一定成立。
难点在边界。1972年，Horn 和 Jackson 找到一个类似熵的函数，沿反应只降不升，系统像球往山谷滚。可当某种物质浓度趋近于零，坡度也趋近于零，球可能卡在边界上。论文举例：2A ⇌ A+B，如果 A 耗尽，正逆反应都停了，边界上的 (0,T) 也成了一个“平衡点”。要排除这种假终点，得先证明每种物质都不会真的耗尽——这叫持久性。这一步，卡了半个世纪。
10月22日，BitMiracle AI Lab 在 arXiv 挂出一篇23页论文。它证明：对满足细致平衡的反应网络——每一对正逆反应在平衡时各自打平——同一个守恒总量下只有一个正平衡点，从任何正浓度出发都会走到那里。严格地说，还要加上速率按浓度幂次计算、速率常数全为正这些条件。arXiv
Claude Opus 5.5 定路线，136个 GPT 6 Astra 写证明、写 Lean 代码、编译、读报错、再改，Lean 4 内核逐步检查。 11天，80多个 Lean 文件。第6天，执行智能体报告教科书那条路要先补的地基太多；决策智能体换了条路，第二天卡住的一步编译通过。知乎
但“50年圣杯被攻克”得往回收一点。论文在“与已有工作的关系”里写明：存在性、唯一性和那套熵方法都是经典的，数学家 Craciun 的证明已经覆盖了本文的情形。 这篇的新意，是另一条更直接、更初等、从持久性到收敛全程机器检查的路线。其中，持久性部分直接建立在 OpenAI 在9月25日公开的定理和71个 Lean 模块上。arXivGitHub
AI 不是第一次证明它；它把一个已知结论，做成了机器可逐步验收的完整证明链。人类作者定题、把关、核对 Lean 命题和数学定义的对应；论文明确，AI 不是作者。11天也不是从零开始。
回到中学课堂，那句话没有变。变的是我们知道它有多重：课本给的是山谷底的风景，数学家要证明的是，从山上任何一个位置出发，球都不会卡在半路的假谷底。这次，机器把这条路从头到尾走了一遍。
