微软研究院证明 KLS 猜想：人类引导智能体探索，独立证明与 Lean 4 验证

2026/10/22 00:10

核心事实：微软研究院研究员 Xinzhi Zhang 与合作者证明 1995 年提出的 Kannan–Lovász–Simonovits（KLS）猜想。该猜想认为，对一大类高维概率分布，最佳平面切割与任意形状最佳切割的面积差不超过一个与维度无关的通用常数。
方法路径：研究者采用人类引导的智能体搜索流程，探索超过 100 条候选路径；AI 系统负责探索数学可能性、执行推导、准备手稿与内部证明检查，研究者负责确定方向、筛选思路、组装最终论证并验证证明。作为对照，多个前沿模型在无引导、相近 token 预算下未达成目标。
验证情况：作者发布完整证明同日，另一组研究者发布了并行完成的完整证明，第三份证明也于同日出现；随后有 Lean 4 形式化版本发布。作者还缩短了证明并在 Lean 中验证，计划最终审查后公开。
行业意义：KLS 此前被视作高维几何、概率论与理论计算机科学的核心开放问题，其解决使一批此前以该猜想为前提的结果可以无条件陈述。该案例也给出一种可核对的人机协作科研形态：AI 扩大搜索与推导规模，数学判断仍由研究者承担。