GPT-5.6 助力证明凸优化 30 年未解难题
UC Berkeley 博士研究生 Phillip Kerger 利用 OpenAI GPT-5.6 Sol Pro 证明了凸优化领域一个自 1996 年悬而未决的问题。相关论文已发表于 arXiv,首次在无梯度凸优化中建立了近乎匹配的复杂度下界 Ω(d²/log d)——此前下界仅为 Ω(d),而上界来自 Protasov 1996 年的 O(d² log² d) 算法,两者之间的差距长达 30 年。
Kerger 在论文中详细记录了 AI 的使用过程:初始提示经过精心设计,模型经过 148 分钟处理生成了初始证明;随后第二轮会话在 230 分钟思考后进一步完善了精度。整个初始证明已用 Lean 形式化验证,确保正确性。论文明确写道:“现代 AI 工具被广泛用于建立本文的结果。”
这一成果的独特之处在于它不是大公司的内部项目,而是一名独立研究者将 AI 作为数学合作者的实践。当模型不仅能理解 10 页的数学上下文、还能产出经形式化验证的原创证明时,AI 对科研范式的改变正在从辅助工具走向真正的智力合作者。