微软研究院证明 KLS 猜想并展示人机协作数学突破

微软研究院研究员 Xinzhi Zhang 与合作者证明了提出于1995年的 Kannan-Lovász-Simonovits (KLS) 猜想，确立了 log-concave 分布的普适几何原则。该成果通过人类指导的 agentic 搜索过程实现，AI 探索了超过 100 种候选方案，研究者负责评估与剪枝，最终消除了维度依赖。目前已有多个独立团队验证该证明，并发布了 Lean 4 形式化版本。