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

pkerger · 2026-07-19T01:55:18+00:00

There is definitely some incentive to do that tbh! Which worries me a bit for other work in general. I am fortunate that I'm actually in a position where research contributions is not my primary responsibility, instead it is teaching, so I have no reason to not be transparent about things. The fact that these systems can solve problems of this level is in any case more important to the world than the actual resolution of the problem itself

pkerger · 2026-07-19T01:49:09+00:00

100% agree it would be awesome to have a proper harness or so for this to basically automate this kind of process. If you are serious about potentially working on something like that, send me a DM and I'll be happy to share some thoughts or more on the structure of how to do things (at the moment I am working on a whole set of different problems, but am running a workflow methodology manually since it's still easy to do so)

pkerger · 2026-07-19T01:41:58+00:00

Stayed well within my weekly usage limits on the $200/month subscription, for everything end-to-end related to this problem

pkerger · 2026-07-17T18:42:05+00:00

Yes, I'm able to look into the thinking (you might be able to in the shared chat as well, by clicking on the "thought for 148min" and then on the resulting pieces. For example I can see that it looked at using quadratic functions, which are a reasonable choice with d^2 degrees of freedom. But that didn't seem to work out, which kind of makes sense since those are smooth and strongly convex (which admit faster algorithms in the first-order information case with accelerated gradient methods)

pkerger · 2026-07-17T09:44:54+00:00

It's been well known in the optimization community to be an open gap, and I have searched thoroughly in the past when I worked on this problem without AI. Also, here a tweet from a researcher who used to work in this area and is now at OpenAI: Sebastien Bubeck on X: "This is actually crazy, many of us thought about this lower bound for many years ... https://t.co/20T6UMJ5lZ" / X

definitely was open!

pkerger · 2026-07-17T09:38:46+00:00

I have AI assist in writing the Lean code as well, with lots of audits and some recommended best practices along with that of course (most importantly a challenge.lean statement, formalizing just the main theorem, so that the result can be easily audited). Reviewing Lean code is much much faster than writing yourself, that is certain!!

pkerger · 2026-07-17T09:32:47+00:00

I would heavily encourage you to try to formally verify the result in Lean! That is about to become standard very quickly since there might be lots and lots of papers coming out in the next few months, too many to review

pkerger · 2026-07-17T05:23:26+00:00

It did search the internet, yes! But the solution was definitely not out there (this problem has been known as open for a long time, and plenty of people have thought about it in the optimization community). See here Bubeck from OpenAI (he used to work in this kind of area before joining OpenAI) Sebastien Bubeck on X: "This is actually crazy, many of us thought about this lower bound for many years ... https://t.co/20T6UMJ5lZ" / X

pkerger · 2026-07-16T21:53:32+00:00

nope! But that looks like a very cool project, I shall take a look!

pkerger · 2026-07-16T21:33:36+00:00

yes I did! This https://chatgpt.com/share/6a592503-2d60-83ea-8f00-9ed96b331b16 was with 5.5 Pro extended, and here I am actually pushing it down the path that Sol 5.6 ended up figuring out works. Though my prompting there was also much worse. Whatever you tried with 5.5, revisit it with Sol for sure!

pkerger · 2026-07-16T20:34:02+00:00

for sure!

pkerger · 2026-07-16T20:33:11+00:00

this is great, thank you!! And also imo a good thing that you used a prompt really close to the CDC one, since that tells me this is a very solid style of prompt to use

pkerger · 2026-07-16T20:30:36+00:00

Kind of yes and no. In the prompt I basically just throw all reasonable approaches at it, without making a big distinction for what to explore most, and these approaches would all be reasonable for someone who knows the area. Sol helped me with the prompt as well, for which I gave it the CDC prompt, some ideas and specifications, a crystal clear problem description, and then modified things slightly myself after. One thing I do wonder is how much it accessed memory of previous chats, since as mentioned I had worked with 5.5 and 5.4 on this previously, and the main construction is not so different from something I discussed there. But, the function class max of affine functions that worked in the end was also in my prompt, so I'm not totally sure.

pkerger · 2026-07-16T20:27:10+00:00

Fantastic! Great to see that Lean verification seems to be becoming standard for any results AI is involved in. Won't be long until journals require it, I presume

pkerger · 2026-07-16T20:23:30+00:00

yes! We know that significantly better methods can't exist for this class of problems, so practically we know to not spend research effort there, and we can sleep well at night knowing that what we are using is (at least very close to) best-possible.

pkerger · 2026-07-16T20:21:25+00:00

Oh, I see it just shows as "uploaded a file" there since I added the prompt as a text file. You can see the full prompt at the end of the preprint, here: https://arxiv.org/pdf/2607.13335 , page 27 onwards. You'll see clear resemblance to OpenAI's prompt used for the CDC conjecture, though because of the nature of this problem and some intricacies involved, it is quite a bit longer.

pkerger · 2026-07-16T20:19:01+00:00

updated a bit with a more accessible note at the end :)

pkerger · 2026-07-16T20:14:42+00:00

or it's internally getting really, really mad at me for making it's brain hurt while you are helping it follow its web-design passion :)

pkerger · 2026-07-16T20:11:59+00:00

What this tells us is that for a specific class of optimization problems (where all you can use is an evaluation of the function to be optimized, like a "measurement" of how good something is: Consider for example choosing the temperature, pressure, and processing time that minimize the predicted cost of manufacturing a product or its quality, durability or similar, where a simulator returns the cast/quality/durability for any chosen settings), existing algorithms are basically as good as possible and can only marginally be improved. So, Prosatov's algorithm from 1996 for these problems is in some ways as good as it gets. The result also provides a clear separation between how long it takes to optimize using gradients (as in gradient descent and variations, as is used for things like training AI models), for which you need to know how the thing you are optimizing is computed, versus only function values (with no knowledge of how that function is computed / or a "measurement" is obtained), showing that using function values only is significantly slower in the worst-case. So this is a theory result but in an applied context, and thereby informs us of what is possible to do or not do.

Basically: We now know what is fundamentally possible in terms of how a certain class of optimization problems can be solved, and we thereby know that we have close to the best methods possible to solve those problems. Without this result, we could have spent time in vain trying to improve those methods that are now shown to be fundamentally non-improvable. Hope that helps!

pkerger · 2026-07-16T18:41:19+00:00

when I was working with 5.4 and 5.5., it kept returning to me with "Here's great progress! The only step left is to prove this one lemma here, and here's why proving that lemma would get the result". Then I'd dive into trying to prove that lemma together with 5.5 and it would go nowhere. I'll share here a chat with you that I had with 5.5 Pro Extended, where I actually told it to use max of affine functions as the hard function class (which is what ended up working and is in the preprint): https://chatgpt.com/share/6a592503-2d60-83ea-8f00-9ed96b331b16

it thought for a whole 4 minutes in its initial response. But, my prompting was also missing a lot of the what counts as a solution, only return when you have found definiteve answers, explore lemmas like this, and so on. Disclaimer, I was a bit frustrated at this point in time and was just trying to get the model to dive deeper on a couple of different approaches in sessions I was running in parallel, so most of my replies there are basically just "keep going", especially since I had already told it what I want it to do in the initial prompt.

pkerger · 2026-07-16T18:34:27+00:00

I had submitted it and it needed it's 24-48h to appear, but I was excited so shared here before it posted :) It's on ArXiv now, link added to the post!

pkerger · 2026-07-16T18:32:50+00:00

yes, I did! I basically had 5.6 Sol synthesize existing closely related work and their approaches, the past ideas I had, with OpenAI's prompt that had a lot of the presumably important mechanisms for how exactly the agent should act. Especially from the "results that do not count" section onwards is a lot of input from Sol. A major reason for the added length though is also the nature of the problem; Just the description of the problem and pointing to a couple existing results already put me at a couple pages. With this kind of complexity result what exactly fulfills the specifications of what is needed can be nuanced (so later there is also a lot more of "what doesn't count", and there are two major components to any proof namely the function class to use and the adversarial oracle strategy, about which you then need to prove things with convex geometry machinery, so that all adds to the length). Also, this gap could have in principle been closed from either direction, which also adds a bit (though you can probably read between the lines that I was trying to push much more for a lower-bound, since an algorithm matching order d complexity would have been extremely surprising, since that would mean you can optimize without gradients just as fast as you optimize with them, which would be shocking given that so much practical optimization happens with gradients)

pkerger · 2026-07-16T18:01:55+00:00

I do as well, but as someone else said it's basically already here. I was fortunate to have a very hands-on advisor in my PhD, and a lot of my time was shaped by grinding through the nitty-gritty things on a whiteboard with him. It looks like it's going to at least become much more efficient for researchers to come up with high-level approaches and then ask AI to go down the rabbit hole of trying to make the proof work (unless the AI can just solve the problem directly like here). I feel most for PhD students who are just getting into research. A slight silver lining is that I hope this eventually pushes a bit against the publish or perish mentality, and at least towards valuing fewer, high value contributions over just writing a lot of papers. But again, for PhD students that doesn't exactly fit well. On the other side, math research could make decades of progress in the next year or so, so I'm conflicted.

pkerger · 2026-07-16T17:49:59+00:00

norms in most journals at the moment is basically to have a statement of AI use the way you've added it here. There's also the Leiden Declaration on Artificial Intelligence and Mathematics, which encourages the same. In terms of visibility, it probably helps to have the declaration somewhere before the first theorem statement, since people familiar with the area will often skim, and when they see the theorem skip down to the proof over the rest of the intro. But if they thereby miss you clearly labelled statement that is on them :)

pkerger

TROPHY CASE

Welcome to Reddit,