微软研究院证明 31 年未解的 KLS 猜想
微软研究院的 Xinzhi Zhang 与合著者证明了 1995 年提出的 KLS 猜想，确认高维对数凹分布中最优平面切割与任意形状切割的效果只差一个与维度无关的常数。作者在人类主导的智能体搜索流程中探索了 100 多条候选路径，由研究者筛选和调整方向，最终借助递归改进与误差有界证明完成证明。同期另有独立团队给出完整证明，并有 Lean 4 形式化验证发布。
推荐理由：微软研究员用人类主导的智能体搜索证明 KLS 猜想，展示了人机协作做数学研究的具体分工方式。