KLS 猜想 31 年后被证明：人剪枝、Agent 铺路

微软研究院 10 月 21 日（美国时间）发文，Zhao Song 和 Xinzhi Zhang 用一批 AI Agent 证明了 1995 年提出的 KLS 猜想。博客里还放了一组对照：同样的 token 预算，让几个顶尖模型自己去证，都没走完。同一天还有另外两份独立证明出现，作者也写明大量用了 AI。

31 年的难题，卡在一个 log 上

KLS 猜想说的是：对任何各向同性的对数凹分布，Poincaré 常数（或者说 Cheeger 常数的倒数）有一个跟维度无关的上界。它连着高维采样随机游走的混合速度、凸体体积算法的复杂度，还有凸体的中心极限定理，是凸几何和理论计算机里的老问题。

这些年进展一直是一点点挤：Chen 2021 年做到 n^o(1)，Klartag 2023 年做到 √log n，今年 7 月 Letwin 的预印本把 ψ_n 推到 O(log^1/4 n)。离「跟维度无关」只差最后这点 log，可这点 log 卡了好几年。

人管方向，Agent 管铺路

微软的博客把分工写得很具体。AI Agent 负责探索候选思路、推公式、写证明草稿，也做内部的证明检查；两位研究者决定往哪走、挑哪些想法留下，最后自己核验整份证明。他们一共试了 100 多种候选方法，人一轮轮剪掉走不通的。

时间线也在 arXiv 上：v1 发布于 10 月 1 日 10:43（UTC），标题是 O(4^{log* n}) 的界；v2 在 10 月 4 日 21:21（UTC）更新，标题改成「An O(1) Bound for the KLS Constant」。从迭代对数到常数，中间只隔了三天。

对照组用了差不多的 token，几个顶尖模型各自去证，都没到终点。

整篇博客里，这组对照最值得细看。微软没有公布用的是哪些模型，也没给具体 token 数，只说预算「大致相同」。所以它能说明的是：在这道题上，人做剪枝明显比放手让模型跑更有效。它说明不了哪家模型更强。

同一天冒出三份证明

巧的是，Bizeul、Klartag、Lehec 在同一天贴出了另一份完整证明（arXiv 2610.05474），走的是累积量加「suspension」的路线。他们在致谢里写得很直白：多数证明和数学思路是 ChatGPT 找到的，suspension 这一步是作者自己提的。

第三份来自 Balasubramanian 和 Kasiviswanathan（arXiv 2610.07728），给出确定性的变分证明，把 Poincaré 常数压到 25 以内。论文专门有一节「AI Usage Statement」，说证明是在多个前沿模型的大量协助下做出来的，作者逐条核验过。

能不能信：形式化先跑在前面

140 页的分析证明，评审要花很久。开源仓库 KLS500 先给了一层机器检查：用 Lean 4 证明了 Poincaré 常数不超过 500，说明里写着重新构建了 1,710 个数学模块，公理检查只出现 propext、Classical.choice、Quot.sound 三个标准公理。它主要依据第二篇的思路，也用到了 Song 和 Zhang 的一个判据。

Lean 证明也有边界：常数 500 比论文里的界松，仓库也写明 Comparator 和 Nanoda 两个独立检查器没跑。微软说会在评审后发布精简版证明和 Lean 形式化。在那之前，三篇都只是预印本，还要等数学界一行行去审。

最后

做 Agent 的团队可以照这个分工抄一遍：让模型并行铺开方案，人只做两件事，砍掉走不通的路，以及对最后结果负责。想看原文的话，从微软博客读起，再对照 arXiv 2610.01447 的 v1 和 v2，就能看到界是怎么一步步压下来的。