On July 10 — the day after GPT-5.6 Sol Ultra became generally available — OpenAI posted a PDF to its CDN claiming to be a proof of the Cycle Double Cover Conjecture. The model is listed as the sole author. The proof is reportedly three pages.
The Cycle Double Cover Conjecture is not obscure within graph theory. It asks: for every bridgeless graph (one with no single edge whose removal disconnects it), does there exist a collection of cycles such that every edge appears in exactly two of them? George Szekeres posed it in 1973. Paul Seymour posed it independently in 1979. Fifty-some years of professional mathematicians haven’t closed it.
The difficulty isn’t conceptual vagueness — the statement is clean and easy to understand. The problem is structural. Any proof has to work for all bridgeless graphs, including “snarks”: cubic graphs that can’t be properly 3-edge-colored. Snarks are the hard cases, and they’re what make the CDC resistant to the kinds of finite reducibility arguments that worked for the Four Color Theorem. A minimal counterexample to the CDC would have to be a snark with girth at least 12, but snarks with arbitrarily high girth exist, so you can’t enumerate your way out of the problem. The conjecture also sits in a tangle of related open problems — Tutte’s nowhere-zero 5-flow conjecture, the circular embedding conjecture — and proving any of them would have downstream consequences.
So either this PDF is a significant mathematical result, or it isn’t.
What OpenAI actually did
The setup, per OpenAI’s announcement and a post from Ethan Knight, was an agentic harness running 64 parallel subagents from Sol Ultra. The whole thing took under an hour. The Hacker News thread surfaced a few things worth noting about the prompt: it was long and detailed, with explicit meta-instructions telling the model to avoid terminating prematurely and to prefer broad search strategies over greedy depth-first approaches. One commenter observed that a substantial fraction of the prompt “is spent essentially telling the model to actually solve the problem” — which is a slightly uncomfortable observation for a system advertised as having improved intent understanding.
That’s not a knock on the result itself, if it holds. Proof search is genuinely hard, and having a model that can do sustained exploration across 64 concurrent threads — rather than giving up or circling — is exactly what you want. The prompt engineering is doing something real: it’s shaping the search. Whether that constitutes “the model proved it” or “humans and the model jointly produced a proof” is a question worth sitting with, but it doesn’t change whether the proof is correct.
What we don’t know: how many times the harness ran before producing this output, what fraction of attempts produced coherent-but-wrong proofs, and how much human review went into the released PDF. OpenAI hasn’t disclosed any of that.
The verification question is the whole story right now
A PDF on a company’s CDN is not a peer-reviewed proof. Graph theorists are going to spend the next several weeks reading this carefully. The CDC is old and hard enough that the community will bring genuine scrutiny, not just skim it for obvious errors.
The three-page length is interesting. A short proof of a long-open conjecture can go two ways: it’s either elegant (something genuinely was overlooked) or it has a gap that looks superficially plausible but breaks on close inspection. Short proofs of the CDC have appeared on arXiv before — 2015, 2018, others — and none has survived expert scrutiny. That’s the base rate going into this one.
The fact that the proof is machine-generated doesn’t change the verification requirement; if anything, it raises new questions. LLMs can produce text that looks like valid mathematical reasoning but contains subtle non-sequiturs. Unless the proof was produced inside a formal verification system like Lean or Coq — which the announcement doesn’t claim — “machine-verified” means the subagents checked each other’s reasoning, not that a proof assistant confirmed every step.
This is still worth paying attention to. If it does hold up, it’s a meaningful data point about what multi-agent systems can do on unsolved research mathematics — not competition problems, but real open conjectures. AlphaProof’s 2024 IMO results were impressive but those problems had known solutions; this would be structurally different. And even if this particular proof has a gap, the fact that a plausible three-page argument emerged from an hour of compute is non-trivial signal about where the capability frontier is.
The math community’s response over the next few weeks is the only thing that actually matters here.