微软研究员及合作者证明提出31年的KLS猜想

Microsoft Research 于2026年10月21日宣布，其机器学习与优化小组高级研究员Xinzhi Zhang与合作者Zhao Song利用由人类主导的智能体式AI研究流程，证明了Kannan–Lovász–Simonovits猜想。这一问题提出于31年前，属于高维几何与概率领域。

猜想及新的界

证明发表于一篇长达140页的论文《KLS 常数的 O(1) 上界》，作者为Zhao Song和Xinzhi Zhang。论文于2026年10月1日首次提交至arXiv，并于2026年10月4日修订，提交作者为Zhang。摘要称，作者证明KLS常数ψ_n的上界是一个普适常数C，从而解决了这一猜想；他们还证明，每个各向同性对数凹概率测度的Poincaré常数都有一个普适上界。

从形式上说，这一猜想于1995年提出，它要探究的是：n维空间中的每个各向同性对数凹概率测度，其切比雪夫常数是否都有一个普适的正下界。用Microsoft Research博文中更通俗的话来说，对于一大类高维概率分布，最佳平面切分是否总能达到与任意形状的最佳切分几乎相同的效果，两者的差异不会超过一个普适常数，且不受维数影响。由于切分的几何形状决定了随机游走探索某一分布的速度，这一猜想在高维采样理论中占据核心地位。

在这项工作之前，已知的最佳结果是Brayden Letwin于2026年7月27日提交的21页论文《KLS 常数为 O(log^{1/4} n)》。该论文证明ψ_n至多为log^{1/4} n的某个常数倍。Microsoft Research的博文指出，随着维数增加，这一上界仍会缓慢增长。新研究则给出了一个固定上界，不随维数变化。

这一猜想在解决之前早已受到广泛重视。博文记载，Mathematical Sciences Research Institute在2017—18年度报告中称KLS是高维凸几何中的核心未解问题；Simons Institute称其为凸几何领域最重要的未解问题之一；Ronen Eldan则在2022年国际数学家大会的会议录中指出了它的广泛影响。

由人类主导的智能体式研究流程

博文称，作者首先着手改进2026年7月的研究结果。在一个由人类主导、结构化的AI智能体研究流程中，他们探索了100多种候选方案，其中许多涉及高阶张量的冗长计算，并提出了一项新的数学判据，成为最终证明的基础。

随后，作者发现可以递归地应用这一判据：将每次改进后的界重新代入同一论证，从而得到更紧的界。在论文2026年10月1日的版本中，这种做法将对维数的依赖降至迭代对数级别。迭代对数增长极其缓慢，但仍会随维数增加，因此当时还不足以解决这一猜想。最后一步是重复整个递归细化过程，而不是只应用一次。博文称，这一思路受到作者此前关于线性规划快速算法的研究启发。作者证明，每一阶段引入的小误差衰减得足够快，因此误差总和仍受一个与维数无关的普适常数约束，最终在2026年10月4日的版本中完成了证明。

博文指出，递归方法、对该方法的反复应用以及有界误差论证，都是研究人员的原创贡献。AI工具协助探索候选方案、开展详细推导、准备论文稿件并进行内部证明检查；研究人员则决定数学研究方向、筛选有前景的想法、将其整合为最终论证，并验证证明。博文将这一方法描述为一种智能体式搜索，并通过人类参与的迭代筛选不断优化：多个智能体并行探索某个想法的不同变体时，研究人员会检查中间结果、淘汰没有前景的方向，并将最有希望的结果交给下一轮。关键突破出现之前，研究团队大约探索了一百条研究路径。

在项目的另一条独立研究线上，作者曾多次尝试在没有引导的情况下，使用若干领先的AI模型解决同一问题，所用token总预算与主要研究流程大致相同；博文称，这番努力未能达成目标。博文指出，最终取得成功，既依赖AI系统的能力，也离不开研究人员的数学判断。博文感谢Song对这项工作的贡献，并感谢Victor Reis和Ishai Menache在整个项目期间参与讨论。

独立证明与机器验证

2026年10月4日，也就是完整证明发布的同一天，Pierre Bizeul、Boaz Klartag 和 Joseph Lehec 发布了一份平行开展的32页证明，题为《展示 Kannan-Lovász-Simonovits 猜想的一种证明》。论文的摘要指出：“证明中的关键步骤，是 Song 和 Zhang 最近提出的一项判据，该判据涉及倾斜平均的高阶导数。”论文的 arXiv 评论还提到，其中有一段文字描述了人工智能的使用情况。摘要将 KLS 与 Bourgain 切片问题和方差猜想并列，称它们是近几十年来推动高维几何领域数学进展的重要力量。

Krishnakumar Balasubramanian 和 Shiva Kasiviswanathan 发布了另一份独立证明，题为各向同性对数凹测度的庞加莱常数无维数依赖上界；该论文于2026年10月6日首次提交，并于2026年10月8日修订。摘要将其描述为一种确定性的变分证明，为任意各向同性对数凹概率测度的庞加莱常数给出了明确的上界25。

随后出现了名为KLS500的 Lean 4 形式化项目，它形式化证明：对于每个各向同性对数凹概率分布，庞加莱常数都不超过500，且这一上界与维数无关。根据代码库的说明，该项目主要基于 Bizeul、Klartag 和 Lehec 的累积量与悬挂方法，并结合了 Song 和 Zhang 的倾斜—谱判据；验证过程中，在内核信任级别为零的情况下重新构建了1,710个数学模块。Lean 验证也通过了 OpenAI 定义的精确 KLS 猜想表述，该表述采用普适庞加莱常数500。该项目采用 Apache 2.0 许可证。

Microsoft Research 的帖子称，独立证明是数学领域最有力的验证方式之一，因为它们表明一项结果并非依赖单一的推理链条。帖子指出，随着这一猜想得到解决，此前将其作为假设依据的结果如今可以无条件地表述。作者已经缩短了证明，并在 Lean 中验证了精简后的论证；帖子还称，他们计划在最终审查后发布这两者。