A graph theory problem that sat open since the 1960s. A general-purpose language model. Sixty-four subagents working in parallel. Less than one hour on the clock.
That is how OpenAI attributed a proof of the Cycle Double Cover (CDC) conjecture to GPT-5.6 Sol Ultra in July 2026. The Hacker News thread hit the front page within hours. Wikipedia noted the claim the same day. Mathematicians started reading.
I build agent systems for clients, not pure graph theory. Still, this release matters because it pairs the same multi-agent pattern we use in coding with a machine-checkable certificate. The scarce skill is no longer "can the model guess?" It is "can you verify fast enough to ship?"
What the conjecture actually asks
Picture any network of nodes and edges where removing one edge does not disconnect the graph. That is a bridgeless graph.
The CDC conjecture asks: can you always find a multiset of cycles so that every edge appears in exactly two cycles?
Mathematicians believed "yes" for roughly fifty years. Nobody could close the proof. Partial results piled up for planar graphs, certain cubic graphs, and graphs without a Petersen subdivision. The general case stayed open.
The conjecture sounds like abstract combinatorics. It sits in the same research neighborhood as the four-color theorem and snark theory. When a named problem this old falls, people pay attention even before journals catch up.
How OpenAI ran the proof
OpenAI published three artifacts worth studying:
| Artifact | URL | Why it matters |
|---|---|---|
| Proof PDF | cdc_proof.pdf | Three-page argument attributed to GPT-5.6 Sol Ultra |
| Prompt PDF | cdc_prompt.pdf | Shows how OpenAI framed the search problem |
| Lean repo | openai/cdc-lean | Machine-checkable formalization with no sorry placeholders |
The proof strategy, in plain language:
- Reduce to cubic graphs (standard in CDC work).
- Apply the Jaeger eight-flow theorem to get a nonzero group labeling on edges.
- Convert that labeling into a two-element edge assignment at each vertex.
- Close with a short linear algebra check.
The PDF states plainly: "The proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex (with GPT 5.6 Sol)."
The parallel piece is the headline number. OpenAI ran up to 64 subagents concurrently. Wall-clock time landed under one hour. That is the same parallelism story as agentic coding, pointed at a fifty-year math standoff.
Why Lean 4 is the trust layer
LLM math has a credibility problem. Models skip steps and sound confident while being wrong. A PDF on a CDN is not peer review.
Lean changes the verification economics. If the formalization builds, the encoded theorem holds under Lean's logic. OpenAI shipped cdc-lean so outsiders can compile the result without trusting a press release.
That pattern showed up weeks earlier in OpenAI's ten Lean-certified math results, which I covered in Astra's $2,000 math run. CDC is a different problem, but the guardrail is the same: publish the checker.
The honest caveat: Lean verifies formal correctness under Lean's axioms. It does not replace expert review that the formalization matches the mathematical question humans care about. As of mid-July 2026, the proof had not appeared in a refereed journal. Read it as a verified claim, not settled history.
Connection to the Crouzeix proof a week later
OpenAI's CDC prompt became a template. When Dr. Shanmu Jin proved Crouzeix's conjecture in a 16-hour ChatGPT Work session, he adapted the same constraint structure: no web access, branching subagents, adversarial audits, closure only when a complete proof survives checking.
I wrote about Jin's run in A neurosurgery resident solved Crouzeix with ChatGPT. CDC and Crouzeix are different fields, but the harness shape repeats. Deny easy retrieval. Force diverse branches. Audit each other. Run long.
What builders should steal
1. Parallelism is the product feature. Sixty-four subagents is not a benchmark gimmick. It is how you search a large proof space without serializing on one attractive dead end.
2. Publish prompts and certificates. OpenAI put the CDC prompt and Lean repo on GitHub. In client work, that means versioned artifacts, not chat logs. The PR diff and green tests are your certificate.
3. Separate generation from verification. The model proposed. Lean (and human graph theorists) check. Your agent pipelines need the same split.
4. Price the run. CDC did not ship a dollar figure like Astra's $2,000 ten-pack, but the unit economics metaphor still applies. What does one verified agent task cost you?
Useful references:
The takeaway
Whether CDC becomes textbook material or needs a fix, the workflow is already here: parallel subagents, public prompts, Lean certificates. That is closer to how I want production AI to ship than another leaderboard point.
If you are wiring multi-agent research or verification loops into a product, book a free discovery call and we can map the harness to your stack.