Philip Kerger, who teaches industrial engineering and operations research (IEOR) at UC Berkeley, just used GPT 5.6 Sol Pro in chat(!) to one-shot prove a problem in convex optimisation that had stumped him after sporadically working on it for a year or so, and that other researchers had tried and failed at (“only last year at a the ICCOPT conference I heard someone say “we have no idea” how to solve this”). Here’s the chat producing the initial proof after 148 minutes, follow-up chat refining it after 230 minutes, GitHub with Lean code and more, etc.
Kerger’s problem description from reddit
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.
What caught my eye was Kerger’s 10-page(!) effortprompt, available in Appendix A.1 of his paper, inspired by but significantly longer than OpenAI’s own effortprompt behind their proof of the cycle double cover conjecture:
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)
5.6 Sol was a lot better than 5.4 and 5.5 at this, although the effortprompt probably helped a lot
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.
It cost him 10% of his $200 Pro plan (with the initial 5h/day cap)
Between $20 to $200 depending for me depending on how you want to look at it. I got the $200/month subscription specifically to try tackling some problems together with AI.
This specific project used under 10% of my weekly limit on there (though OpenAI messed with limits, increasing them, during this project, so I’m not sure if that’s 100% accurate). Total time was about 2.5h 5.6 Sol Pro use on the initial proof outline, 4h 5.6 Sol Pro on an improvement on the accuracy requirement, ~2h use of verifications and proof audits, ~4h use assisting for the Lean development (these later ones are estimated, and only the time of the actual active tool use, whereas the total time including my own work was of course much more). So something on the order of no more than 15h of actual time.
Even with the initial 5h cap per day they had (and then lifted), that uses 3 days = 10% of the monthly pro plan, so from the user side I can in some way say about $20 (though probably OpenAI’s compute cost much more than that!), or the $200 since I did get the pro plan for this.
As a point of reference, it cost Google DeepMind’s Gemini 3.1 Pro-based agent a few hundred dollars per proof of the 9 open Erdős problems it autonomously solved out of the full set of 353 in the open-source Formal Conjectures repo, with predictably very large variance:
As before, Sol’s proof didn’t really use nor create new techniques:
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.
But frankly I don’t think this is needed for even Fields-level contributions. To quote my own quick take:
Think about what a (static!) automated Jean Bourgain-toolkit interpolator could do
What’s the most impressive research-y feat interpolating AIs can theoretically do, fixing their training data to (say) today?
I don’t have a good sense of this in general, but in pure math it’s probably at least Fields medal-tier, if laudatios like that of Akshay Venkatesh are anything to go by:
Akshay Venkatesh stands out for the startlingly original way he has connected number theory problems to deep results in other areas. Far from using them as “black boxes” to crank out solutions, Venkatesh brings fresh insights to the results and highlights their unexpected connections to number theory. In this way he has made striking advances in number theory while also greatly enriching other branches of mathematics.
This, and the rest of the laudatio, reads like a very souped-up version of what OpenAI’s recent internal model did with Erdos problem #90 (itself a souped-up version of what GPT-5.4 Pro did with problem #1196), give or take a few Gowers-hints. One of Venkatesh’s advantages over other top-tier mathematicians is his sheer range, the thing frontier models do vastly better than humans at.
And I can imagine, for instance, 2 years of advancements enabling a frontier model to skillfully deploy the late legendary Jean Bourgain’s toolkit. Bourgain was regularly spoken of by other world-leading mathematicians as “effectively a god”. Terry Tao:
When I was a graduate student in Princeton, Tom Wolff came and gave a course on recent progress on the restriction and Kakeya conjectures, starting from the breakthrough work of Jean Bourgain in a now famous 1991 paper in Geom. Func. Anal.. I struggled with that paper for many months; it was by far the most difficult paper I had to read as a graduate student, as Jean would focus on the most essential components of an argument, treating more secondary details (such as rigorously formalising the uncertainty principle) in very brief sentences.
Tao goes on to describe Bourgain’s style and toolkit:
I began to realise that Jean had a certain collection of tools, heuristics, and principles that he regarded as “basic”, such as dyadic decomposition and the uncertainty principle, and by working “modulo” these tools (that is, by regarding any step consisting solely of application of these tools as trivial), one could proceed much more rapidly and efficiently. By reading through Jean’s papers, I was able to add these tools to my own “basic” toolkit, which then became a fundamental starting point for much of my own research. Indeed, a large fraction of my early work could be summarised as “take one of Jean’s papers, understand the techniques used there, and try to improve upon the final results a bit”.
In time, I started looking forward to reading the latest paper of Jean. I remember being particularly impressed by his 1999 JAMS paper on global solutions of the energy-critical nonlinear Schrodinger equation for spherically symmetric data. It’s hard to describe (especially in lay terms) the experience of reading through (and finally absorbing) the sections of this paper one by one; the best analogy I can come up with would be watching an expert video game player nimbly navigate his or her way through increasingly difficult levels of some video game, with the end of each level (or section) culminating in a fight with a huge “boss” that was eventually dispatched using an array of special weapons that the player happened to have at hand.
Imagine unleashing thousands of Bourgain-toolkit interpolators math-wide in 2028. I think I’m being conservative here, not assuming continual learning or whatever, not even assuming anyone else’s toolkit, and yet I still find it hard to imagine how transformative this would be. And this is just for pure math.
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.
those lower fruits give the shorter mathematicians the nutrients they need to grow!
It’s wild that this is possible while at the same time my impression with Fable and GPT-5.5 (and predecessors) is that they say roughly one dumb thing per output.
Philip Kerger, who teaches industrial engineering and operations research (IEOR) at UC Berkeley, just used GPT 5.6 Sol Pro in chat(!) to one-shot prove a problem in convex optimisation that had stumped him after sporadically working on it for a year or so, and that other researchers had tried and failed at (“only last year at a the ICCOPT conference I heard someone say “we have no idea” how to solve this”). Here’s the chat producing the initial proof after 148 minutes, follow-up chat refining it after 230 minutes, GitHub with Lean code and more, etc.
Kerger’s problem description from reddit
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.
What caught my eye was Kerger’s 10-page(!) effortprompt, available in Appendix A.1 of his paper, inspired by but significantly longer than OpenAI’s own effortprompt behind their proof of the cycle double cover conjecture:
Snippets of his effortprompt
Page 4 -- vibes-wise this reminded me of Eliezer’s old post referencing The Open-Source Wish Project, Wish For Immortality 1.1
Final page:
How did he come up with such a prompt? With Sol’s help of course
Kerger (paragraphs mine):
5.6 Sol was a lot better than 5.4 and 5.5 at this, although the effortprompt probably helped a lot
It cost him 10% of his $200 Pro plan (with the initial 5h/day cap)
Kerger (paragraphs mine):
As a point of reference, it cost Google DeepMind’s Gemini 3.1 Pro-based agent a few hundred dollars per proof of the 9 open Erdős problems it autonomously solved out of the full set of 353 in the open-source Formal Conjectures repo, with predictably very large variance:
As before, Sol’s proof didn’t really use nor create new techniques:
But frankly I don’t think this is needed for even Fields-level contributions. To quote my own quick take:
Think about what a (static!) automated Jean Bourgain-toolkit interpolator could do
What’s the most impressive research-y feat interpolating AIs can theoretically do, fixing their training data to (say) today?
I don’t have a good sense of this in general, but in pure math it’s probably at least Fields medal-tier, if laudatios like that of Akshay Venkatesh are anything to go by:
This, and the rest of the laudatio, reads like a very souped-up version of what OpenAI’s recent internal model did with Erdos problem #90 (itself a souped-up version of what GPT-5.4 Pro did with problem #1196), give or take a few Gowers-hints. One of Venkatesh’s advantages over other top-tier mathematicians is his sheer range, the thing frontier models do vastly better than humans at.
And I can imagine, for instance, 2 years of advancements enabling a frontier model to skillfully deploy the late legendary Jean Bourgain’s toolkit. Bourgain was regularly spoken of by other world-leading mathematicians as “effectively a god”. Terry Tao:
Tao goes on to describe Bourgain’s style and toolkit:
Imagine unleashing thousands of Bourgain-toolkit interpolators math-wide in 2028. I think I’m being conservative here, not assuming continual learning or whatever, not even assuming anyone else’s toolkit, and yet I still find it hard to imagine how transformative this would be. And this is just for pure math.
those lower fruits give the shorter mathematicians the nutrients they need to grow!
It’s wild that this is possible while at the same time my impression with Fable and GPT-5.5 (and predecessors) is that they say roughly one dumb thing per output.