KLS 完整证明已有论文、平行证明和 Lean 4 形式化；AI 参与部分是人类引导的多路径搜索。
研究者借助人类引导的 AI 搜索证明 KLS 猜想
2026-10-04已核实动态WATCH
研究者证明了提出 31 年的 Kannan–Lovász–Simonovits 猜想，消除了高维采样理论中的维度依赖上界。微软参与的证明由研究者引导约 100 条 agent 搜索路径；同日还有两份平行证明，之后又出现 Lean 4 形式化，构成相互独立的数学核验。这个结果证明了人机协作流程有效，不等于无人引导的模型能独立解决同类问题。
对你意味着什么
对科研 agent 团队来说，这是“机器广搜、人类剪枝、形式化核验”流程的一条强证据。系统设计应暴露中间路径和待证明条件，而不只统计最终答案。
证据与关联材料
技术细节与六维评分
| 结果 | 完整证明 KLS 猜想并得到与维度无关的上界 |
|---|---|
| 工作流 | 约 100 条 AI 研究路径，由人类反复剪枝 |
| 独立核验 | 同日出现两份平行证明；之后发布 Lean 4 形式化 |
| 限制 | 据 Microsoft 披露，相同 token 预算下的无人引导运行没有找到证明 |
| 时间依据 | 证明论文于 2026-10-04 首次公开；官方回顾于 2026-10-21T16:00:00Z 发布 |
技术影响 5
工程价值 3
采用信号 2
成熟度 2
验证成本 4
风险 2