GPT-5.6 solves a 30-year open problem in convex optimization, verified in Lean

[00:00:00]Here's another instance of AI automating mathematics. This is posted on Reddit by P Kerger after OpenAI's CDC proof announcement. GPT-5.6 used a similar prompt to close a 30-year gap in convex optimization verified in Lean.

[00:00:18]I'm Dr. Samuel Allen Alexander, mathematician and philosopher. Still here reading this Reddit post by P Kerger.

[00:00:27]Too long, didn't read. In a single 148-minute session with a prompt modeled after the one OpenAI used to prove CDC, GPT-5.6 Soul Pro supplied a proof that closed a complexity gap in convex optimization that has existed since 1996.

[00:00:45]The result was formally verified in Lean.

[00:00:47]Links to everything and thoughts on AI capabilities are at the bottom of this post.

[00:00:52]Disclosure, I am the author of the preprint and Lean repository linked below. I have a PhD in applied mathematics and am a a teaching prof in IEOR at UC Berkeley. The result has not yet been peer-reviewed.

[00:01:07]Following the recent announcement that GPT-5.6 Soul 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 Soul Pro produced the main argument for a lower bound that I had been unable to prove myself. A lot of my past work has been proving complexity lower bounds in different settings.

[00:01:34]The problem concerns deterministic zeroth-order convex optimization.

[00:01:38]Let B D be the Euclidean unit ball in real D space and consider all convex one-Lipschitz functions F from such ball to the reals.

[00:01:49]An algorithm may query any point X in this unit ball and receives only the exact real number f of x, no other information, but the algorithm knows that f is convex and Lipschitz.

[00:02:02]The algorithm is otherwise completely unrestricted and can use unlimited computation and memory.

[00:02:07]These function value only problems arise naturally when an objective is evaluated through a physical experiment or simulator.

[00:02:15]One can imagine choosing d engineering parameters and observing only the cost returned by the simulation.

[00:02:21]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.

[00:02:39]Let Q of d epsilon denote the worst case number of queries required to find an epsilon optimal point of f.

[00:02:45]An algorithm due to Protassov from 1996 shows that order d squared function evaluations are sufficient, which gives Q of d epsilon equals big O of d squared, an upper bound on the complexity.

[00:02:57]Lower bounds were practically nonexistent for this setting, and the strongest previously applicable bound was only big omega of d, inherited from the stronger first order Oracle model, where the algorithm receives both function values and gradients.

[00:03:10]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.

[00:03:20]And so there was a linear gap in d in the complexity of this fairly fundamental convex optimization setting since 1996.

[00:03:27]So, can you find an algorithm that is better than Protassov's that better than Protassov's and only needs d evaluations?

[00:03:34]Or can you show that no such algorithm can exist and we can sleep well at night knowing that Protassov's algorithm using d squared evaluations is best possible?

[00:03:42]What 5.6 solved proved is the latter.

[00:03:45]I [clears throat] 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.

[00:03:52]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.

[00:04:05]After seeing OpenAI's CDC result, I wrote a much more elaborate prompt following the same general methodology.

[00:04:12]My prompt is about 10 pages long and attached at the end of the preprint. See collection of links below.

[00:04:17]There's a lot baked into this prompt on approaches to try and also on how to how exactly the model should proceed, but it's built exactly in the style of OpenAI's CDC prompt.

[00:04:28]One note is that I gave it a relatively small error requirement to prove the quadratic lower bound under order D to the fourth accuracy.

[00:04:36]After 148 minutes, uh that's D to the minus four accuracy.

[00:04:42]After 148 minutes, GPT-5.6 sole pro returned a proposed proof resolving the quadratic dimension dependence at accuracy of order D to the minus three.

[00:04:52]After checking things myself, I formally verified the proof in Lean and it passed the formal verification check.

[00:04:57]The construction and domain invariant used also make genuine sense to me and are closely related to some other results in complexity of convex optimization. For example, Nemirovski and Yudin's tight bound for first-order convex optimization also uses constructions that are maxes of affine functions.

[00:05:13]Lastly, some important comments about the work relating to AI capabilities.

[00:05:18]In a lot of cases, proving lower bounds like this result relies on finding the 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.

[00:05:36]There are only so many function classes which would be reasonable to look at.

[00:05:40]Here, quadratics, for example, would have also been reasonable with order D squared degrees of freedom or any variation of maxes of some simpler families of convex functions as well.

[00:05:49]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.

[00:06:08]So, I wouldn't really say that this result is using or creating some fundamentally new techniques in convex geometry or optimization theory.

[00:06:16]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 or theoretical computer science will be made obsolete, but I think it will instead no longer make sense to work on any low-hanging or even medium-hanging fruit. We'll be needed for problems where actual novel approaches are needed.

[00:06:39]I agree with that 100%.

[00:06:41]The author then gives a bunch of links.

[00:06:43]Links to pre-print, readme code, complete prompts, proof map, and build instructions.

[00:06:49]In a pre-print at the archive, the original uninterrupted 148-minute chat that produced the initial proof, the later chat that led to the data the minus one half power refinement, OpenAI's CDC prompt that I structured things after, and a more accessible account I wrote on Medium.

[00:07:09]Edit. This was Soul Pro, not Ultra. I had been working in Codex before this, where the level above X High is Ultra.

[00:07:17]But, I did this in the web interface, where the highest is Pro, which is in fact not quite the same as Ultra.

[00:07:24]Very interesting. It seems as though the floodgates have been opened, and now automated mathematical and computer science results are starting to pour in.

[00:07:35]But, I do agree with P Kerger's closing comment that we probably will not see mathematicians and computer scientists, at least at the high levels, put completely out of job.

[00:07:48]Low-hanging and medium-hanging fruit will probably all get annihilated, but humans will, at least in the short term, still be needed for work which requires fundamental new types of mathematics.

[00:08:02]I'm Dr. Samuel Allen Alexander, mathematician and philosopher. Please like, comment, and subscribe, and I'll see you in the next video.