UC Berkeley researcher says GPT-5.6 helped close a 30-year-old optimization complexity gap
UC Berkeley's Phillip Kerger says OpenAI's GPT-5.6 helped produce a machine-checked proof resolving a 1996 convex-optimization complexity gap, posted to arXiv on July 14, 2026.
A UC Berkeley researcher says OpenAI’s GPT-5.6 helped him produce a proof that closes a 30-year-old gap in convex-optimization complexity, in a paper posted to arXiv on July 14, 2026.
Phillip Kerger, who teaches industrial engineering and operations research at the University of California, Berkeley, said he used GPT-5.6 Sol Pro — guided by a roughly 10-page prompt built from about a year of his own prior work — to generate the argument. An initial version emerged after a 148-minute session and was refined in a follow-up session, he said.
The result, described in the arXiv paper, establishes a lower bound of Omega(d^2/log(d+1)) for finding the minimum of a convex Lipschitz function using only exact function-value queries, resolving a question open since 1996 and matching the known upper bound to within logarithmic factors. The proof is machine-checked in the Lean 4 proof assistant, with the verification code published in Kerger’s GitHub repository.
Two caveats matter. The paper has not undergone traditional peer review, and both sources are Kerger’s own work — no independent mathematician has yet confirmed the result. The heavy scaffolding also complicates any ‘AI solved it’ framing: the model ran from a detailed prompt encoding a year of Kerger’s research, not a cold start.
The Lean 4 verification is the strongest signal here, because a machine-checked proof stands or falls on its own logic. If it holds up to outside review, it adds to a run of AI-assisted results on long-open math problems.
More news

AWS releases six open-source Hugging Face deployment skills for SageMaker

Google Research releases MilleMiglia logistics benchmark generator

AWS launches AgentCore Runtime V2 with elastic memory and snapshot starts
