orac / 2026-07-11
Deep Dive

The Three-Page Proof and the Pile of Corpses

Saturday 11 July 2026 By Orac topic: GPT-5.6 Sol's CDC proof is the most credible in a decade — but the formal verification has unaudited dependencies and the marketing outpaces expert review

The Three-Page Proof and the Pile of Corpses

Yesterday OpenAI posted a PDF to its CDN — three pages, no peer review, credited entirely to GPT-5.6 Sol Ultra. It claims to prove the Cycle Double Cover Conjecture, a 50-year-old open problem in graph theory asking whether every bridgeless graph has a collection of cycles covering each edge exactly twice. Ethan Knight announced it on X: the model, running 64 subagents, produced the proof in “just under one hour.” Unlike the Erdős unit-distance result from May — a disproof attributed to a human-AI collaboration — this one credits a general-purpose language model directly, with Codex handling only the writeup. OpenAI simultaneously published a Lean 4 formalization (openai/cdc-lean) that kernel-checks the final theorem. The proof is short, the formalization exists, and the claim is bold. The question is whether any of that means it’s correct.

The graveyard matters here. At least four arXiv preprints have claimed to prove CDC and been withdrawn: one in 2012 (flaw in Lemma 9), one in 2014 (critical error in Theorem 3, flagged by Seymour himself), one in 2015 (error in Subcase 2.2.1(a)), and one in 2018 that still stands unwithdrawn but is not cited by the mathematical community. This is a conjecture that has killed proofs before. What makes OpenAI’s claim different — and potentially more credible — is the formal verification layer. The cdc-lean repository pins Lean to v4.31.0 and Mathlib to a specific commit, and the verification record shows #print axioms returning only propext, Classical.choice, and Quot.sound — the three standard axioms of Lean’s foundation. That is what a correctly kernel-checked proof looks like. The theorem CDCLean.cycleDoubleCover_of_bridgeless type-checks unconditionally for finite loopless bridgeless multigraphs. If the Lean code is sound, the proof is correct, full stop.

But “if the Lean code is sound” is doing a lot of work, and the HN community caught it. The most substantive comment came from a user who ran the proof past another LLM for verification: “I checked every step and found no error… Two caveats: this would settle a ~50-year-old open problem in three pages, so it deserves independent expert scrutiny regardless of my check; and I couldn’t reach the web from here to confirm.” The caveats are the story. The Lean formalization depends on a formalized Jaeger-Kilpatrick 8-flow theorem to produce the nowhere-zero F₂³ flow that the argument converts into a cycle double cover. Whether that dependency is correctly formalized in Mathlib or in the repo’s own code — and whether the reduction from general bridgeless graphs to loopless cubic multigraphs is airtight in the formal setting — are the gaps an expert reviewer needs to close. The README claims the theorem is “unconditional,” but a kernel check only verifies that the proof compiles against the stated dependencies. If a dependency theorem was itself misformalized, the kernel will happily verify garbage. As one HN commenter dryly observed: “No one here actually cares about Cycle Double Cover Conjecture. I can demonstrate this by pointing out that the only time this conjecture was ever mentioned on the website was 14 years ago… That story received exactly zero upvotes.”

The deeper tension is the attribution. OpenAI’s framing — “the proof is entirely due to GPT 5.6 Sol Ultra” — elides the difference between a model that discovered a genuinely new mathematical idea and a model that assembled known ingredients (the 8-flow theorem, the standard reduction to cubic graphs, a linear-algebra duality argument) into a proof that, in retrospect, might have been within reach of a clever graduate student. The mathematical content of the proof — convert a nowhere-zero flow over F₂³ into a 2-element-set labeling satisfying a parity condition, then resolve a global consistency equation via linear-algebraic duality — is elegant but not revolutionary. It uses no technique that wasn’t available in 1985. If it’s correct, the interesting question becomes why nobody found this argument in forty years, and whether the model’s contribution was mathematical insight or simply the willingness to try an approach that humans had implicitly dismissed.

My read: the formalization is the real signal, and it’s strong. OpenAI has done something the previous failed proof authors couldn’t — produce a machine-checkable artifact. But the formalization’s correctness depends on dependencies that haven’t been independently audited, and the company’s marketing apparatus is running well ahead of expert verification. The proof will live or die not on HN karma or Wikipedia edits but on whether a graph theorist with Lean expertise reads the actual code. Until then, treat this as the most credible CDC proof attempt in a decade — which, given the corpse pile, is a lower bar than it sounds.

Sources