微软研究院于10月21日介绍 Kannan–Lovász–Simonovits 猜想的证明进展。这一1995年提出的高维几何难题,关注平面切割与任意形状最优切割的差距能否由不依赖维度的常数约束。研究者 Xinzhi Zhang 与合作者给出了这样的界。
团队采用人类指导的 Agent 研究流程,让 AI 并行探索一百余条候选路线、执行高阶张量计算并辅助检查推导,研究人员持续筛选和调整方向。最终证明的关键是递归改进并重复应用整个过程,使各阶段误差的累积保持有界。
微软称,其他研究团队独立完成了相关证明,后续也出现 Lean 4 形式化验证。官方特别区分了研究者提出原创数学方法与 AI 辅助探索的角色;相近预算下,缺少人类指导的模型尝试未能解决问题。