微软研究团队10月21日介绍,研究者与合作者完成了Kannan–Lovász–Simonovits(KLS)猜想的证明。这是一个自1995年以来悬而未决的高维几何与概率问题,结果对随机采样、优化和相关算法理论都有意义。
这项进展并非模型独立解题。研究者采用人主导的代理式探索:AI代理并行尝试候选路径,研究者检查中间结果、淘汰无效方向并决定下一步;约探索了100条研究轨迹。微软称,AI还协助推导、整理稿件和内部检查,但数学方向、关键思路组合以及证明核验由研究者完成;同等Token预算下的非定向模型尝试没有解决问题。
官方还提到,独立团队同期给出了完整证明,后续也出现Lean 4形式化工作。值得关注的不是“AI单独证明了猜想”,而是人在环路中的搜索、筛选与验证如何帮助推进高难度研究。
来源:Microsoft Research(2026-10-21)
https://www.microsoft.com/en-us/research/blog/solving-a-31-year-old-grand-challenge-in-mathematics-the-kls-conjecture/ |