UC Berkeley数学教授Phillip Kerger用GPT-5.6 Sol Pro在148分钟内证明了一个自1996年悬而未决的凸优化下界。证明已用Lean形式化验证。他花了约10页篇幅写prompt，包括问题描述、失败思路和验证规范。
凸优化中有一个悬了30年的问题：在只能查询函数值、拿不到梯度信息的情况下，找到一个ε最优解到底需要多少次函数查询？
1996年，Protasov证明O(d²)次查询足够了(d是维度)。但下界一直停留在线性Ω(d)，这意味着理论上可能存在比d²快得多的算法。这个"线性缺口"成了该领域的痛点。
UC Berkeley的Phillip Kerger教授用GPT-5.6 Sol Pro一次性解决了它。在一个148分钟的对话中，AI完成了证明，证实d²确实是必需的下界——没有任何算法能打败Protasov的方案。证明已在Lean定理证明器中通过形式化验证。
核心prompt大约有10页长。Kerger在其中详细描述了问题、建议尝试的思路、以前失败的方向、构成有效证明的规范，甚至用GPT-5.6自己去合成相关工作和prompt指引。他借鉴了OpenAI的CDC(计算发现与验证)prompt方法论。
证明的关键结构是使用"仿射函数的最大值"这一函数类，这与Nemirovsky和Yudin在1983年给出一阶优化紧确下界的经典方法有关。
Kerger对此的评价很务实：这个结果使用的都是现有技术，真正的挑战在于找到正确的构造和对策oracle策略。他认为，"如果一个结果用现有技术可以达成，现代AI方法就能解决它。"他预计研究者不会被淘汰，但"再去碰低垂甚至中等高度的果实已经没有意义了。"
原文：https://old.reddit.com/r/math/comments/1uxj3cy/after_openais_cdc_proof_announcement_gpt56_used_a/