GPT-5.6 drops a 60-year-old graph theory proof. Now what?

What happened

OpenAI dropped a PDF on their CDN over the weekend: a claimed proof of the Cycle Double Cover Conjecture, generated by GPT-5.6 Sol Ultra. The Hacker News thread hit 447 points in a few hours, which is roughly what happens when a model claims to have cracked something mathematicians have circled since 1973.

The conjecture itself is easy to state and famously hard to prove: every bridgeless graph has a collection of cycles such that every edge appears in exactly two of them. Szekeres posed it in 1973, Seymour independently in 1979, and it has sat on the shortlist of "embarrassingly simple to state, brutal to prove" problems in combinatorics ever since. Partial results exist — proofs for specific graph classes, reductions to snarks, connections to the four color theorem — but the general case has resisted every human attack for half a century.

The PDF is 187 pages, written in what looks like standard journal-style LaTeX, and cites 94 papers. It routes through a construction the authors (well, the model) call "stratified compatibility systems," which extends the Alspach-Zhang framework in a way that's either genuinely novel or a very convincing hallucination. As of publication, no working mathematician has signed off on it, and the OpenAI blog post accompanying the release is characteristically careful: the word "proof" appears in quotes exactly once.

Why it matters

This isn't the first time an AI system has claimed a major result. DeepMind's AlphaProof got silver-medal-equivalent scores at IMO 2024, and there have been half a dozen "AI proves X" headlines in the last eighteen months. Most of them dissolved on inspection. A 2025 preprint claiming a novel Ramsey bound turned out to have a gap on page 41 that a graduate student found in an afternoon. The pattern is familiar: model outputs something that *looks* like a proof, and then the community spends weeks figuring out whether it actually *is* one.

What's different this time is the length and the specificity. 187 pages is long enough that spot-checking won't cut it — you need someone to actually work through it. And graph theory is a small enough community that we'll know within a month whether the construction survives contact with people like Bojan Mohar or Carsten Thomassen. Early reactions on MathOverflow are cautiously interested. One commenter wrote: "Lemma 4.7 is either the cleverest thing I've seen this year or completely wrong, and I genuinely can't tell yet." That is, in fact, the whole story.

The deeper issue is epistemological. When a model can generate a 187-page proof in a few hours, the bottleneck moves from *producing* mathematics to *verifying* it — and human verification does not scale. Lean, Coq, and Isabelle are the obvious answer, and OpenAI hints in the accompanying post that a machine-checked version is "in progress." But formalizing a 187-page combinatorics proof is itself a multi-month project. The Kepler conjecture proof took Hales and his team over a decade to formalize. If Sol Ultra is churning out claimed results faster than the formalization community can keep up, we're going to end up with a growing pile of "probably true" theorems in a limbo state that mathematics has never had to reason about before.

There's also a career-industry angle worth naming. Graduate students in combinatorics just watched a language model take a swing at their thesis-generator problem. Whether or not this specific proof holds, the message to anyone starting a PhD in a discrete-math-adjacent field is unambiguous: the low-hanging fruit is going to get eaten. The interesting research questions in the next five years will not be "can we prove X" but "can we verify that the machine's proof of X is correct, and if so, what does the proof teach us that we didn't already know?"

What this means for your stack

Most readers here are not going to formalize a graph theory proof this week. But the workflow question generalizes. If you're building anything that relies on AI-generated outputs whose correctness matters — code, contracts, medical summaries, security policies — the Sol Ultra release is a preview of the verification tax you're about to pay.

Right now, "the model wrote it, ship it" is a defensible position for a lot of low-stakes work. That posture ages badly the moment your model starts producing outputs your team can't fully audit in the time available. The mitigation is the same one mathematicians are converging on: build machine-checkable representations of your correctness criteria, and route model outputs through them before they touch production. In software, that means property-based tests, formal specs where you can afford them, and treating model-generated code the way you'd treat a pull request from a very fast, very confident junior. In non-code domains, it means the same thing with different vocabulary: structured schemas, validators, and a human review budget scaled to consequence rather than volume.

The practical takeaway: if your team hasn't started thinking about how to grade AI outputs at 10x current throughput, start now. The graph theorists are about to run this experiment publicly, in slow motion, and whatever they figure out about triage — what to check first, what to trust provisionally, when to walk away — is going to be directly applicable to everyone shipping AI-touched work.

Looking ahead

Sol Ultra's proof will either survive the next six months of scrutiny or it won't. Either outcome is interesting. If it holds, we've got a working template for AI-assisted resolution of open problems, and every math department in the world is going to be rethinking its research pipeline by fall. If it collapses, we've got a very expensive object lesson in why verification infrastructure is the actual bottleneck, and the next round of "AI proves X" announcements will land with a lot more skepticism. Either way, the interesting work in the next year is not going to be the models — it's going to be the checkers.