AREX Feed Article
微软研究院宣布解决 31 年悬而未决的 KLS 猜想，同月已有三篇证明与机器验证
北京时间 10 月 22 日凌晨，微软研究院（Microsoft Research）官方 X 账号 @MSFTResearch ：几十年来，高维计算挑战中一个关键问题始终得不到证明，而新研究已经解决 KLS 猜想，“移除了理解科学与计算中广泛使用的随机算法效率的一大障碍”。帖文发布于协调世界时 10 月 21 日 16 时 11 分，短链指向研究院，标题直书主题——《Solving a 31-year-old grand challenge in mathematics – the KLS conjecture》（解开一个 31 年历史的数学大挑战：KLS 猜想）。
被宣布解决的 KLS 猜想于 1995 年提出。证明出自 Zhao Song 与微软研究院机器学习与优化组（Machine Learning and Optimization group）的 Xinzhi Zhang：论文《An O(1) Bound for the KLS Constant》于 10 月 1 日提交至预印本平台 ，10 月 4 日的更新版本给出完整证明，全文 140 页，摘要写明由此“解决 KLS 猜想”（resolving the KLS conjecture）。同样在 10 月 4 日，Pierre Bizeul、Boaz Klartag 与 Joseph Lehec 提交了；10 月 6 日，出现；一个把猜想写成机器可检验定理的 也已在 GitHub 公开。
一条凌晨发帖，和它背后的 arXiv 论文
帖子本身只有两句话，内容在链接背后。博客在 “At a glance” 一栏把这项工作概括为四点：解决了被广泛视为高维几何核心未解问题之一的 31 年难题，影响统计学、优化、算法与计算机科学；确立了对数凹分布的一条普适几何原理——简单的平面切口能以固定倍数捕捉它们最窄的瓶颈，与维数无关；突破来自一个由研究者主导的智能体式（agentic）过程；多名独立研究者已验证这项研究，其核心判据被认作关键突破，随后还完成了机器检验的形式化验证。博客副标题则写道：微软研究员与合作者结合新的数学思想与人类引导的 AI，解决了高维几何与概率中的一个核心问题。
论文本身可以在 arXiv 上完整核对：分类为数学·概率（math.PR），提交人为 Xinzhi Zhang，作者栏列出 Zhao Song 与 Xinzhi Zhang；博客说明 Xinzhi Zhang 来自微软研究院机器学习与优化组，并在致谢部分把 Zhao Song 称为合作者。摘要先复述猜想的问题——R^n 上每个各向同性对数凹概率测度，是否都有不依赖维数的普适正常数 Cheeger 常数下界——随后写明：作者证明了 KLS 常数 ψ_n ≤ C（C 为普适正常数），并给出同样普适的 Poincaré 常数上界。
把凸体对半切开：平面切口够不够好
KLS 猜想问的是一道切分题。把一个高维凸体（convex body）的体积对半分开，切口可以是平面，也可以是任意弯曲的曲面。给出的表述是：KLS 断言，超平面在所有凸体中至多差一个常数因子，就几乎是最优的“最稀疏切割”（sparsest cut，即分开单位体积所需边界最小的切法）。微软研究院博客的版本更直白：对一大类高维概率分布，最好的平面切口与任何形状的最优切口之差不超过一个普适常数，与维数无关。博客的示意图给了一个具体例子：正四面体上，对半分割的平面切面面积为 0.2500，而允许任意曲面时最小切面约 0.2173，相差约 15%；猜想说，无论凸体是三维的正四面体还是一千维的什么形状，这类差距永远不会超过一个固定倍数。
Simons 的文章说，猜想最初来自估计凸体体积的 MCMC（马尔可夫链蒙特卡洛）算法；博客则解释，切口的几何决定随机游走探索一个分布有多快，KLS 因此在高维抽样理论中处于中心位置。写道，KLS “位于统计学与计算机科学许多问题的核心”——比如热量在凸体中扩散需要多久，或者随机游走者要走多少步才能到达真正随机的位置。Weizmann Institute 的高维几何学家 Ronen Eldan 当时告诉 Quanta，随机游走几乎是唯一有效的抽样方法，而许多计算机科学问题中“算法最重要的子程序，就是采一个随机点”。
31 年里，部分结果不断收窄缺口，但完整证明始终缺席。Simons 的文章记录：2019 年，Yin Tat Lee 与 Santosh Vempala 借助 Ronen Eldan 引入的 stochastic localization（随机局部化）技术，把缺口缩到 O(n^(1/4)) 因子；随后 Yuansi Chen 又把它推进到亚多项式的 n^(o(1))。今年 7 月 27 日，华盛顿大学数学系的 Brayden Letwin ，超过了此前最佳的 O(√log n)。在这份新工作之前，最好结果仍是 7 月的这个界——缓慢增长，但不是常数。Simons Institute 的另一句评价是：“凸几何中最重要的未解问题之一”。
约一百条研究轨迹：递归收紧与人工“剪枝”
按博客的叙述，证明分三步。第一步是改进 7 月的结果，把界做得更精确。搜索在一个由人主导的智能体式过程中展开：多个 AI 智能体并行探索同一个想法的变体，研究者审阅中间结果、砍掉没有前途的方向、把最有希望的结论递给下一轮——博客把这轮人工筛选称为“剪枝”（pruning）。探索过的候选思路超过 100 种，许多涉及高阶张量的冗长计算；约一百条研究轨迹之后，一个新判据浮现，成了最终证明的地基。
第二步是一个发现：判据可以递归使用。每轮把刚得到的更紧的界喂回同一个论证，就能推出更紧的下一轮；在 10 月 1 日的版本里，这把对维数的依赖压到了迭代对数（iterated logarithm）——一个增长极慢、但毕竟随维数增长的函数。离完全解决还差一步。
第三步是把整套递归再迭代一遍，灵感来自两位作者此前在线性规划快速算法上的工作：他们证明了每一轮引入的小误差衰减得足够快，总和始终被一个与维数无关的普适常数罩住。10 月 4 日更新的版本由此完成证明。博客写明了分工：递归方法、它的反复应用、误差有界的证明是研究者的原创贡献；AI 工具负责探索候选思路、完成细节推导、准备手稿、执行内部证明检查。
博客还留了一个对照：在项目的另一条线上，作者用大致相同的 token（词元）总预算，反复让多个前沿 AI 模型无引导地求解同一个问题，未能达到目标。博客写道，最终的成功既依赖 AI 系统的能力，也依赖研究者的数学判断。
同日出现的第二篇证明，和常数 500 的机器验证
独立确认来得很快。10 月 4 日，就在 Song 与 Zhang 提交完整证明的同一天，Bizeul、Klartag 与 Lehec 提交了他们独立发展的完整证明；其摘要明确写道，证明的关键一步正是 Song 与 Zhang 最近提出的关于 tilt averages 高阶导数的判据。三人的摘要还把 KLS 与 Bourgain 切片问题、方差猜想并列，称其为近几十年高维几何发展的驱动力。
10 月 6 日，Krishnakumar Balasubramanian 与 Shiva Kasiviswanathan 提交第三篇证明，路径不同：先建立维数无关的 Poincaré 不等式，再推出 KLS 猜想。这篇论文的附录给出一个显式常数——普适 Poincaré 常数不超过 1 + 2×10¹⁶。博客对多份证明并立的意义有一句解释：“独立证明是数学中最强的验证形式之一，因为它们表明结果并不依赖单条推理链。”
再往后是机器验证。GitHub 上名为 KLS500 的仓库（10 月 8 日更新）把猜想的形式化表述变成了 Lean 4 中可检验的定理：每个各向同性对数凹概率测度满足 Var(f) ≤ 500∫‖∇f‖² dμ，并由此得到 Cheeger 常数的普适下界。按仓库自述，它主要基于 Bizeul 等人的 cumulant–suspension 方法，纳入 Song 与 Zhang 的关键判据，再作量化改进，把常数压到 500——而最优的普适 Poincaré 常数被夹在 4 与 500 之间。验证重建了 1,710 个数学模块，只依赖 Lean 的三条标准公理（propext、Classical.choice、Quot.sound）。
从“假设成立”到“无条件成立”
对领域而言，这份证明改变的是结论的条件性。博客的结论写道：此前一大类把 KLS 当假设用的结果，现在可以无条件陈述；凸几何、概率与理论计算机科学由此获得更稳的地基。Simons 的文章在 2021 年就列出过 KLS 成立将直接确认的一串猜想——切片（slicing）猜想、薄壳（thin-shell）猜想、一类中心极限形式。博客把这次的结果概括成一条原理：高维空间比已知更“规矩”，在其中穿行的障碍不会随维数无限增长。
微软研究院同时把这项工作当作方法论样本：博客认为它展示了“人类引导的 AI 协作能够促成真实的科学发现”，且 AI 增强而非取代人的洞见——方向的选择、想法的取舍、最终论证的组装与核验都由研究者完成。这仍是研究院对自家项目的表述；可公开查验的，是三篇 arXiv 证明和那个 Lean 仓库本身。
博客还说，两位作者已把证明精简，并用 Lean 核验了精简版论证，两者都计划在最终审阅（final review）完成后发布。到那时，数学与理论计算机科学社区可以更方便地检验这项猜想的证明，并在此基础上继续搭建。