A PhD in applied mathematics has used OpenAI’s GPT-5.6 Sol to produce a proof that closes a gap in convex optimization theory that had been open since 1996 — the year the author was born. In a single 2.5-hour session, with a 10-page prompt and no human intervention, Sol produced a lower bound on the oracle complexity of deterministic nonsmooth zeroth-order convex optimization. The proof is Lean-verified. Peer review has not happened.
🔍 THE BOTTOM LINE: This is the second publicly documented case in two weeks of GPT-5.6 Sol producing a non-trivial mathematical proof using the long-prompt, multiagent-search technique OpenAI pioneered with the Cycle Double Cover Conjecture. The Lean check confirms the proof is syntactically valid. What it does not confirm is whether the result is interesting, whether the technique generalizes, or whether the next paper is already being written by a model that doesn’t need a 10-page hand-crafted prompt. That is the open question — and it’s the one the HN commentariat spent 193 comments arguing about.
What Was Actually Proved
The problem is in the field of zeroth-order convex optimization. Given a convex function of d variables, where the only thing an algorithm can do is query the function’s value at chosen points (no gradients, no derivatives — just function evaluations), how many queries do you need to solve the problem to a given accuracy?
In 1996, Protasov gave an algorithm that uses on the order of d² evaluations. For three decades, the best known lower bound was only on the order of d — a factor-of-d gap between what was achievable and what was provably necessary. The question: is d² essentially optimal, or is there a cleverer algorithm that gets by with fewer evaluations?
The new result, described in detail by Phillip Kerger, gives a lower bound of d² (up to logarithmic and constant factors). That means Protasov’s 1996 algorithm is essentially the best possible. The gap is closed.
This matters beyond pure math. Zeroth-order optimization underlies simulation-based engineering design, hyperparameter tuning in machine learning, and any optimization driven by physical measurements or human feedback. Knowing that d² queries are necessary tells you when to stop searching for a cleverer algorithm and start engineering around the constraint.
The Prompt Was the Story
The most important technical detail is not the proof — it’s the prompt. Kerger explicitly modeled his approach on the 10-page prompt OpenAI published for the Cycle Double Cover proof. That prompt is not “solve this problem.” It is a ten-page document that primes the model with context, instructs it to use multiagent v2 with up to 64 concurrent agents, demands adversarial self-checking at every step, and specifies exactly which classes of partial progress do not count.
Kerger’s prompt, also published, follows the same pattern: long context, explicit search-management heuristics, adversarial verification baked into the prompt itself. The proof came out in one shot, 2.5 hours, no human intervention. The Lean check took longer to set up than the proof took to generate.
This is the part that should worry — or excite — anyone doing mathematics. The unit of work is no longer “a paper” or “a proof.” It’s “a prompt plus a model plus a verifier.” The bottleneck is moving upstream, from solving to asking.
The Lean Verification Layer
Lean is a programming language for formalizing mathematics. It does not read a proof and decide whether it’s convincing — it mechanically checks that each step follows from the previous ones according to specified axioms and rules. If Lean says a proof is valid, the proof is valid relative to the formalization.
The gap between “Lean-valid” and “mathematically correct” is small but non-zero: the formalization itself can contain errors (the wrong theorem was formalized, an axiom was mis-specified, the statement doesn’t quite match the informal claim). Lean does not catch those. Mathematicians do, in peer review, by reading the informal proof and comparing it to the formal statement.
Kerger acknowledges this explicitly: “we all know that these models are fantastic at bullsh*tting, and producing things that pass the eye test for being correct while being utter nonsense.” The Lean check is the defense against the bullshit. It is not the same as community acceptance.
Why the HN Thread Blew Up
The Hacker News thread hit 327 points and 193 comments in five hours, which is unusual for an r/math cross-post. The arguments fell into four camps:
- The goalpost movers. “Waiting for comments saying that LLMs can’t produce anything new and general goalpost moving.” The pre-emptive strike against dismissal.
- The formalists. “No Mizar no proof.” The position that formal verification is necessary but not sufficient — and that the choice of verifier (Lean vs Mizar vs Coq) is itself a philosophical commitment.
- The metacritics. “The most interesting thing in research is finding new questions, that we understand and that we know why they are important. And that’s something that humans need.” The argument that solving is the easy part; asking is the hard part.
- The cancer-cure crowd. “Cool can we use AI to get a cure for cancer yet? Or is math-turbation the only thing these things are good for?” The impatient utilitarian view, which misses that convex optimization lower bounds are exactly the kind of result that constrains what cancer-drug-discovery optimization pipelines can ever achieve.
The thread is worth reading because it is a real-time record of mathematicians and computer scientists watching the ground shift under them. Two years ago, the argument was “LLMs can’t do real math.” Now the argument is “okay, they can do real math, but that doesn’t count because [reasons].” The [reasons] are getting narrower with each proof.
How This Slots Into the Bigger Arc
This is the third major AI-mathematics story in a month. The Erdős disproof came first, then the Cycle Double Cover proof, now this. The pattern is consistent: a frontier reasoning model, a carefully engineered prompt, a long autonomous search, and a result that would have been a publishable paper if a graduate student had produced it.
What’s changing is the cost curve. The CDC proof required OpenAI’s internal infrastructure and a model (Sol Ultra) that isn’t broadly available. Kerger’s proof used the consumer-accessible Sol model and a hand-written prompt. The technique is diffusing. The next proof will be cheaper to produce than this one.
A separate recent paper on arXiv documents the same pattern from the other direction: a researcher used GPT-5-pro as a collaborator on a convex analysis lemma, and found that the model “accelerated our progress by suggesting relevant research directions and by proving some intermediate results” while “its reasoning still required careful supervision, particularly to correct subtle mistakes.” That was October 2025. Nine months later, the supervision requirement is shrinking and the autonomy is growing.
NZ Angle
New Zealand doesn’t have a Lean-active mathematics research community of any size, but it does have a growing applied optimization community — particularly in logistics, renewable energy grid design, and agricultural systems modeling, all of which lean heavily on zeroth-order and simulation-based optimization. A lower bound that says “d² queries are necessary” is the kind of result that tells an NZ optimization engineer when to stop tuning an algorithm and start redesigning the problem. The practical impact is local even if the proof is global.
The bigger NZ angle is the workforce one. If a model can produce publishable mathematics in 2.5 hours with a 10-page prompt, the value of a graduate student is shifting from “produces proofs” to “writes prompts and evaluates results.” NZ’s universities have not yet reckoned with what that means for PhD recruitment in pure and applied math. They should.
❓ FAQ
Is this proof accepted by mathematicians? No. It is Lean-verified, which means it is mechanically checked against a formalization. Peer review — where mathematicians read the informal proof and assess its interest, novelty, and correctness relative to the formal statement — has not happened. Lean-valid is a strong signal but not the same as community acceptance.
How is this different from the Cycle Double Cover proof? The CDC proof used OpenAI’s internal Sol Ultra model and infrastructure. This proof used the consumer-accessible Sol model and a hand-written prompt modeled on the CDC prompt that OpenAI published. Same technique, lower barrier to entry. The diffusion of the method is the story.
What is zeroth-order optimization and why should I care? It’s optimization where you can only observe the value of a function, not its gradient. It shows up whenever you’re optimizing something you can measure but can’t differentiate — physical experiments, human preference ratings, simulation outputs, hyperparameter tuning. The lower bound says d² measurements are essentially necessary. That’s a floor on how efficient any such optimization can ever be.
Does this mean mathematicians are obsolete? No. It means the part of the job that is “produce a proof of a well-posed conjecture” is being automated. The parts that are not yet automated: identifying which conjectures matter, posing the right questions, evaluating whether a result is interesting, and connecting it to the rest of mathematics. The arXiv paper from October 2025 explicitly notes the model “still required careful supervision” even on a smaller problem.
Where can I read the proof and the prompt? Kerger has published the paper, the Lean verification, the full 10-page prompt, and the initial chat log on GitHub. The OpenAI CDC prompt is also public. Anyone with a Sol subscription can attempt to reproduce the technique.
🔍 THE BOTTOM LINE: A 30-year gap in convex optimization closed in 2.5 hours by a model using a prompt technique OpenAI invented two weeks ago. The proof checks out in Lean. The technique is now in the wild. The next question is not whether models can do mathematics — they can — but how long it takes for the “but peer review” and “but finding questions” defenses to collapse the same way “but they can’t prove anything” already has.
📰 Sources
- Phillip Kerger, “An AI-assisted breakthrough in convex optimization” (Medium, July 2026)
- Hacker News discussion, r/math cross-post (48957779)
- OpenAI, “Prompt used for a proof of the Cycle Double Cover Conjecture” (cdn.openai.com)
- Salim, Adil, “Accelerating mathematical research with language models” (arXiv:2510.26647, October 2025)
- Singularity.kiwi prior coverage: GPT-5.6 Sol Ultra and the Cycle Double Cover Conjecture, OpenAI’s Erdős disproof, ChatGPT solves 42-year math puzzle
