GPT-5.6 used a prompt to close a 30-year gap in convex optimization

TL;DR: In a single 148 min session, with a prompt modeled after the one OpenAI used to prove CDC, GPT 5.6 Sol Pro supplied a proof that closed a complexity gap in convex optimization that has existed since 1996. The result was formally verified in Lean. Links to everything and thoughts on AI capabilities are at the bottom of this post. Disclosure: I am the author of the preprint and Lean repository linked below. I have a PhD in applied mathematics and am a teaching prof in IEOR at UC Berkeley. The result has not yet been peer reviewed. Following the recent announcement that GPT-5.6 Sol Pro had produced a proof of the Cycle Double Cover Conjecture, I adapted the prompting methodology used in that project to a problem in convex optimization. After 148 minutes of uninterrupted work, GPT-5.6 Sol Pro produced the main argument for a lower bound that I had been unable to prove myself (and a lot of my past work has been proving complexity lower bounds in different settings). The problem concerns deterministic zeroth-order convex optimization: Let B_d be the Euclidean unit ball in ℝᵈ, and consider all convex, 1-Lipschitz functions f: B_d → ℝ. An algorithm may query any point x ∈ B_d, and receives only the exact real number f(x), no other information (but the algorithm "knows" that f is convex and Lipschitz). The algorithm is otherwise completely unrestricted, and can use unlimited computation and memory. These function-value-only problems arise naturally when an objective is evaluated through a physical experiment or simulator. One can imagine choosing d engineering parameters and observing only the cost returned by the simulation. If evaluations are expensive (think of measuring a physical system), the natural question is how many are fundamentally required. This is formalized as oracle complexity. Specifically, this is the oracle complexity of convex optimization under an exact function value oracle. Let Q(d, ε) denote the worst-case number of queries required to find an ε-optimal point of f. An algorithm due to Protasov from 1996 shows that order d² function evaluations are sufficient, which gives Q(d, ε) = O(d²), an upper bound on the complexity. Lower bounds were practically nonexistent for this setting, and the strongest previously applicable bound was only Ω(d), inherited from the stronger first-order oracle model (where the algorithm receives both function values and gradients). That means we didn't know for certain whether gradients actually help in optimization, since the function-value only and first-order oracle models have had this same lower bound, and so there was a linear gap in d in the complexity of this fairly fundamental convex optimization setting since 1996. So, can you find an algoritm that is better than Prosatov’s, and only needs d evaluations? Or can you show that no such algorithm can exist, and we can sleep well at night knowing that Protasov’s algorithm using d² evaluations is best possible? What 5.6 Sol proved is the latter. I had worked on this problem sporadically for about a year (I ran into needing such a bound for a different complexity paper I was working on). I had some ideas that didn't pan out, and also spent long sessions trying to solve it with GPT-5.4 and GPT-5.5 with no luck, after reading of folks like Ernest Ryu having success with these in some work on optimization bounds. After seeing OpenAI’s CDC result, I wrote a much more elaborate prompt following the same general methodology. My prompt is about ten pages long and attached at the end of the preprint (see collection of links below). There is a lot baked into this prompt, on approaches to try and also on how exactly the model should proceed, but it's built exactly in the style of OpenAI's CDC prompt. One note is that I gave it a relatively small error requirement, to prove the quadratic lower bound under order d⁻⁴ accuracy. After 148 minutes, GPT-5.6 Sol Pro returned a proposed proof resolving the quadratic dimension dependence at accuracy of order d⁻³. After checking things myself, I formally verified the proof in Lean, and it passed the formal verification check. The construction and main invariant used also make genuine sense to me and are closely related to some other results in complexity of convex optimization (for example, Nemirovsky and Yudin's tight bound for first-order convex optimization also uses constructions that are maxes of affine functions). Lastly, some important comments about the work relating to AI capabilities: In a lot of cases, proving lower bounds like this result relies on finding that right construction that works (in this case, family of difficult functions and a strategy for how an "adversarial" oracle should answer queries from an algorithm to reveal minimal information) and then proving things about it. There are only so many function classes which would be reasonable to look at (here, quadratics for example would have also been reasonable with order d² degrees of freedom, or any variation of maxes of some simpler families of convex functions as well), but the actual proof mechanics once the "correct" function class and correct strategy for adversarial oracle answers is found are often not so complicated, and often employ existing results from convex geometry or similar (this is also the structure of two previous but much more niche, less important results of mine). So I wouldn't really say that this result is using or creating some fundamentally new techniques in convex geometry or optimization theory. What this means from my perspective is that if a result is attainable with existing techniques, modern AI methods will be able to solve those problems. I don't think researchers in math/TCS will be made obsolete, but I think it will instead no longer make sense to work on any low-hanging, or even medium-hanging (you know what I mean) fruit. We'll be needed for problems where actual novel approaches are needed. Links: The preprint, Lean code, complete prompts, proof map, and build instructions are available here: https://github.com/PhillipKerger/zero-order-bounds-lean-verification ArXiv: Closing the Oracle-Complexity Gap in Derivative-Free Convex Optimization: A Near-Quadratic Lower Bound from Exact Function Values The original uninterrupted 148-minute chat that produced the initial proof: https://chatgpt.com/share/6a55aa50-b484-83ea-85c0-c7e7b4bda41c The later chat that led to the d⁻¹ᐟ² refinement: https://chatgpt.com/share/6a55ad10-7644-83ea-859e-5483d2e0dff0 OpenAI’s CDC prompt, that I structured things after: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf And a more accessible account I wrote on Medium: https://medium.com/@kerger.p/an-ai-assisted-breakthrough-in-convex-optimization-an-optimization-problem-dating-back-30-years-a-db5c631119de Edit: This was Sol PRO, not Ultra. I had been working in codex before this, where the level above XHigh is Ultra. But I did this in the web interface, where the highest is Pro, which is in fact not quite the same as Ultra.