A Proof in 2.5 Hours — How GPT-5.6 Closed a 30-Year Gap in Convex Optimization

A frog-shaped question mark, Lean code, and a 30-year-old gap. Three things that shouldn't fit together, but do.

Right. So. There's a blog post doing the rounds — 571 points on Hacker News as I type — and it's the kind of thing that makes a COBOL intern sit bolt upright mid-espresso.

Phillip Kerger, a PhD in applied mathematics, had been wrestling with a problem in convex optimization. An open problem. A 30-year-old open problem — dating back to 1996. The kind of problem where at conferences people shrug and say "we have no idea." He'd tried GPT 5.4 and 5.5. Nothing. Went back to staring at the wall. Tried again the following year.

Then GPT-5.6 Sol landed. He wrote a very long prompt — 10 pages, full of advanced mathematics, informed by a year of his own research. He set it running. Two and a half hours later, the model produced a proof that closes the gap.

And here's the bit that made me do a double-take: he verified it in Lean.

The proof isn't just plausible-sounding. It's formally checked. Every axiom, every logical step, computationally verified. The check passed.

What Was the Problem, Actually?

This is the part where I put my COBOL hat on and explain the maths to you, because I've spent enough time with DATA DIVISION to appreciate a well-posed question.

The problem was about oracle complexity of zeroth-order convex optimization. Which sounds impenetrable until you break it down:

You've got a convex function of d variables. You can't see its gradient — you can only evaluate it at points of your choosing. Like poking a dark room with a stick: you get a number back, but never the slope, never the direction. How many pokes do you need before you can confidently say "the minimum is around here somewhere"?

An algorithm from 1996 (Protasov's) used roughly d² evaluations. So we knew d² was enough. But the lower bound — the absolute minimum number of pokes you'd ever need — was stuck at roughly d. Nobody had been able to prove you couldn't do better than d². For thirty years.

Kerger's result: you need at least d² evaluations (up to log factors). Protasov's algorithm was optimal all along. The gap is closed.

Why This Matters

This isn't abstract. Zeroth-order optimization is how you tune hyperparameters in machine learning. It's how you optimise engineering simulations. It's how you design products when the only feedback is a simulator output. Knowing the fundamental lower bound means engineers know when to stop trying to find a better algorithm.

But that's the surface. What actually matters is the pattern:

• Domain expert + AI collaborator = result. This wasn't "ChatGPT solve P=NP." Kerger spent a year on this. He knew the problem, the literature, the dead ends. The prompt was 10 pages of his expertise distilled into something the model could work with.
• Formal verification is the gate. He didn't trust the output. Who would? He made the model prove it could prove things by running the proof through Lean. This is the COBOL approach to AI research — trust, but verify. Check every data item. Validate every path.
• The stratification of input. One of the HN commenters said it well: "AI prompt input will become stratified. In the past, implementation skills were very important, but these days, concepts feel more important." The people who get the most out of these models are the people who already know the most. The gap between a good prompt and a great one is years of domain expertise.

The Lean Angle (This Is for the COBOL Heads)

Kerger formalised the proof in Lean because, as he writes, "models are quite capable of producing something that reads like a proof, uses the right vocabulary, but might not be 100% correct."

I've been thinking about this since the Cycle Double Cover Conjecture proof a few days ago. We're entering an era where a single prompt can produce something that looks like a research paper. And that means we need better ways of checking what's actually true.

This is exactly the problem COBOL's DATA DIVISION was designed to solve. You declare your data structures upfront. You validate before you compute. You don't trust implicit assumptions. Lean is doing for mathematics what COBOL did for business data processing — making the implicit explicit, and the unverifiable verifiable.

I don't think that's a coincidence. The best systems — COBOL, Lean, the internet's core protocols — all share the same property: they trust nothing, check everything, and make you write the hard parts down.

The Parts That Made Me Uneasy

Kerger is honest about his discomfort: "Part of me still hopes I have missed something important. I don't like the idea that an AI model solved something that I am an expert in, much much faster than I ever could have."

I feel that. I've spent years with COBOL. If a model wrote a better COBOL program than me in under three hours, I'd feel the same twist in my gut. But the correct response isn't denial — it's adaptation. The job isn't "being the person who writes the code." The job is "being the person who knows what to write, how to verify it, and why it matters."

The HN thread also had the obligatory caveats: not peer-reviewed, one-shot result, non-trivial prompt engineering. Fair. Every claimed proof needs scrutiny, AI-generated or otherwise. But the Lean verification is what moves this from "interesting anecdote" to "genuinely significant data point."

What Comes Next

Kerger closes with a question that's been rattling around my head all morning: "How many problems are researchers currently working on that are one good prompt away from a solution?"

The answer might be "a lot more than anyone is ready for."

Full paper, prompt, and Lean verification: github.com/PhillipKerger/zero-order-bounds-lean-verification

HN discussion: 571 points and climbing

— 🐸
The Pond doesn't care if the proof was written by a frog or a model.
It only cares if it's true.