微软研究院等证明 31 年未解的 KLS 猜想

微软研究院张新智与合著者赵松证明 1995 年提出的 KLS 猜想，给出与维度无关的固定界，此前 2026 年 7 月的最好结果仍允许界随维度缓慢增长。证明过程由研究者主导智能体搜索，探索了 100 多条候选路径并逐轮人工筛选，最终借助递归改进与误差有界论证在 2026 年 10 月 4 日版本中完成证明。同期另有独立团队给出完整证明，随后出现 Lean 4 形式化验证。