On July 15, 2026, a post appeared in Reddit’s math community with an unremarkable title — roughly, “After looking at OpenAI’s CDC conjecture proof approach, I tried GPT-5.6 and closed a 30-year gap.”
Three days later, the post had picked up 477 points and 308 comments on Hacker News. Among the mathematicians who had read the Lean code line by line, the verdict was surprisingly uniform: this time, it’s a genuine mathematical contribution.
After working through the discussion, I found the impact comes down to this: it tackled a task that human mathematicians find especially thorny — proving a lower bound. And GPT-5.6 did it in one prompt and 148 minutes.
What happened: one prompt, 148 minutes, a 30-year gap
Phillip Kerger is an assistant professor of applied mathematics at UC Berkeley, holds a PhD in optimization theory from Johns Hopkins, and previously did research at NASA’s Quantum Artificial Intelligence Laboratory. Since last year he’d been chipping away, on and off, at one problem — a complexity gap in convex optimization that had been open since 1996.
Put simply: in 1996 someone designed an algorithm with a complexity of \(O(d^2 \log^2 d)\). Everyone knew you couldn’t do better than \(O(d)\) (since you have to at least glance at every dimension). But the 30-year void between \(O(d)\) and \(O(d^2 \log^2 d)\) went unfilled — was there something faster, or had the old algorithm already hit the wall?
Kerger had tried GPT-5.4 and GPT-5.5 before; both failed. Even when he manually pointed the model toward the right function family, it couldn’t fill in the last few steps.
Then GPT-5.6 arrived.
Following the structure of the “cycle double cover conjecture” proof prompt that OpenAI had published a few weeks earlier, he wrote a roughly 10-page prompt — specifying the mathematical setup, enumerating viable proof routes, packing in lessons from his own failed attempts, and explicitly defining what would not count as a valid solution. He first used GPT-5.6 to help organize the relevant literature and refine the argument scaffolding in the prompt, then fed the final version to the model in a single continuous session.
148 minutes later, GPT-5.6 produced a complete proof construction.
Image: Unsplash / GuerrillaBuzz — a convergence illustration for convex optimization methods. What GPT-5.6 proved is precisely that the lower-bound curve can’t be pushed any lower — the 1996 algorithm was already sitting on the theoretical limit.
The result: a lower bound of \(\Omega(d^2 / \log(d+1))\), separated from the known upper bound of \(O(d^2 \log^2 d)\) by only a logarithmic factor. That rules out the possibility of “a method dramatically faster than the 30-year-old algorithm.”
Why is “proving a lower bound” so much harder? A running analogy
To grasp the weight of this, let me start with an everyday analogy.
Proving an upper bound is like proving you can run 100 meters — you just run it once, stop the clock, and the conclusion holds.
Proving a lower bound is like proving you can’t run faster — for which you have to rule out every possible training method. New shoes? No help. A different starting stance? No help. A special diet? Still no help. To make “you can’t break 9 seconds” hold, you have to exhaust every conceivable approach and show, one by one, that none of them helps.
In mathematics, proving an upper bound (“I found a method that achieves at least this”) is relatively easy — you give an algorithm, compute its complexity, done. But proving a lower bound (“no method can be faster than this”) requires constraining all possible algorithms. You have to prove that no matter how anyone designs a new algorithm, no matter what trick they use, no matter how many detours they take — none of it works, the limit is right here.
That’s why a commenter on HN who goes by alternator — someone who claimed to “know a bit about this area” — put it this way:
“Proving an upper bound is easy, it’s just how long your algorithm ran. Proving a nontrivial lower bound is much harder, because it requires you to constrain all possible algorithms.”
And what GPT-5.6 pulled off this time was exactly the latter. It didn’t just prove that Kerger’s constructed algorithm works well — it proved that the 1996 method had already hit the theoretical ceiling. For 30 years no one could rule out “maybe there’s a better way”; GPT-5.6 ruled it out in 148 minutes.
Two kinds of AI doing math: stop conflating them
When discussing AI doing mathematics, it’s worth distinguishing two things. They look similar but are fundamentally different.
First: AI-assisted conjecturing. This has been happening for several years. Researchers have the model look for patterns among known results, generate “promising-looking” conjectures, and then humans verify them. The model says “I think this inequality might hold,” and a human checks it with pen and paper or a computer. Here, AI is a very smart assistant, but the final judgment rests with the human.
Second: AI independently completing a rigorous proof — and passing formal verification. This is what GPT-5.6 did here. The model didn’t just output a “plausible-looking” argument; the argument was fully translated into Lean 4 — a proof assistant system — and compiled line by line without error. Lean doesn’t accept rhetoric like “obviously” or “it is easy to see.” In Lean’s world, either every step’s logic is airtight, or it throws an error — there’s no middle ground.
Kerger put the entire proof’s Lean code on GitHub. Anyone can install a version manager called elan, clone the repo, run one line of lake build, and watch the compiler run start to finish without error. Run #print axioms and confirm there’s no sorryAx (the placeholder in Lean meaning “I haven’t proven this step yet”) — meaning there are no gaps anywhere in the logical chain.
Kerger’s 36-page preprint, the full prompt, the model conversation logs, the Lean code, the build instructions — all public. This disclosure standard is more than a notch above papers that merely tack on an acknowledgment thanking “AI systems for assistance.”
Image: Unsplash / Bozhin Karaivanov — the Lean proof assistant code interface. GPT-5.6’s proof was fully translated into Lean 4 and compiled cleanly, with no sorry (unproven step) anywhere in the logical chain.
To be fair: the skeptics are worth hearing too
I don’t intend to write this as an “AI crushes humans” puff piece. There was plenty of reasoned skepticism on both r/math and HN, and those voices matter for seeing the whole picture.
First, the field is genuinely niche. Several commenters noted that this convex-optimization lower-bound problem is far less well-known than the “cycle double cover conjecture” OpenAI cracked earlier. The latter is a famous 50-year-old problem in graph theory, while this lower-bound conjecture lives mostly within a relatively small optimization-theory circle. Its academic value is real, but its reach beyond the specialty is limited.
Second, transferability is uncertain. The reasoning pattern that proving a lower bound requires — constraining all possible algorithms — is indeed a high-difficulty category, and GPT-5.6 demonstrated capability here. But can that capability transfer from convex optimization to other branches of math? No one knows yet.
Third, a priority dispute. In the r/math discussion, some people were digging through 1990s Russian optimization literature, suspecting the core lemma in Kerger’s proof may have already been published by Soviet mathematicians — just in journals not commonly indexed by Western databases. If confirmed, GPT-5.6’s contribution becomes “reconstructing an argument from nearly forgotten literature and formalizing it in a way no one had before.” Those are two contributions of different weight.
Fourth, “148 minutes” isn’t the whole story. Kerger had already spent a year on this problem, on and off. That 10-page prompt packed in his understanding of the problem, his failed attempts, the dead ends he’d ruled out. Before GPT-5.6, both GPT-5.4 and GPT-5.5 had failed on the same problem. The 148 minutes was the final uninterrupted proof search — not magic from scratch. As RuntimeWire reported: “the prompt wrapped a year of domain work inside it.”
Image: RuntimeWire / Gemini — an AI-generated illustration of the math proof workflow. Worth remembering: behind the prompt is a year of domain buildup; the 148 minutes was only the search time for the final step.
What really matters is this working model
Setting the controversy aside, the thing here I find most worth watching isn’t the specific theorem at all.
It’s that the human + AI + formal-verification triangle workflow was shown to be reproducible.
Kerger’s method is clear: break the big problem into small lemmas, translate each lemma into a rigorous Lean statement first, then have the model fill in the proof. Whichever lemma fails to compile gets iterated on individually — a change in one place won’t topple the entire proof and force a restart. This workflow doesn’t require you to be a Fields Medalist; the barrier is being able to define your problem precisely.
In other words, there is now an actionable recipe for AI eating “medium-difficulty” math problems. This won’t put mathematicians out of work — defining the problem, constructing the prompt, judging whether the output is nonsense, all of that still requires a human for now. But it will change the daily life of mathematical research: the researcher increasingly acts like a director, and the AI increasingly like the execution team.
One HN commenter put it bluntly: sometimes reading these discussions feels like reading gibberish. But don’t let the jargon scare you — the essence is simple. For 30 years, humans knew how fast an algorithm could run, but couldn’t say “this is the limit.” An AI, guided by a year of one person’s buildup, proved “this is the limit” in 148 minutes. Then another machine called Lean checked its homework line by line and confirmed it took no shortcuts.
That’s the math frontier of 2026 — humans, AI, and proof compilers, starting to work together on one project team.
Reference links:
- Reddit r/math: After OpenAI’s CDC proof announcement, GPT-5.6 used a prompt to close a 30-year gap in convex optimization
- HN discussion (item?id=48957779)
