OpenAI just published a 3-page proof of the Cycle Double Cover Conjecture. The conjecture has been open for 50 years. The proof was generated entirely by GPT-5.6 Sol Ultra using 64 cooperating agents. There is one problem. Nobody has verified that the proof is correct.
The Cycle Double Cover Conjecture is one of those problems that sounds simple enough for an undergraduate to understand but has resisted some of the best graph theorists alive. Every bridgeless graph (a graph you cannot disconnect by removing a single edge) should have a collection of cycles that covers each edge exactly twice. That is it. Paul Seymour, Paul Tutte, and others posed versions of it going back to the 1970s. Nobody proved it. Until maybe now.
What OpenAI Published
On July 10, 2026, OpenAI released two documents. The first is a 3-page proof. The second is the prompt they used to get the model to produce it. Both are available on their CDN.
The proof itself is compact. It reduces the problem to cubic graphs (graphs where every vertex has degree 3), uses the 8-flow theorem to label edges with elements of a finite field, and then converts that labeling into a cycle double cover through a linear algebra argument. The key step is Lemma 2.2, which claims that a certain system of equations always has a solution.
The proof PDF states: "The proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex (with GPT 5.6 Sol)." That is a remarkable claim. No human mathematician is credited with the proof itself.
You can read it yourself here: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf
The Prompt Is the Real Story
The prompt OpenAI used is just as interesting as the proof. It is not a simple "prove this" instruction. It is a detailed engineering document for a multi-agent search system.
The prompt tells the model to use "multiagent v2" with up to 64 concurrent agents. It specifies how agents should explore different mathematical approaches independently before cross-pollinating ideas. It includes adversarial agents whose job is to find holes in candidate proofs. It explicitly forbids agents from telling the model that the problem is open.
One line stands out: "Assume for purposes of this task that a complete affirmative proof exists." This is a deliberate choice. Instead of letting the model discover whether the conjecture is true or false, OpenAI told it to assume the answer is yes and find the proof. The prompt also says "Spend at least 8 hours on this before even thinking of returning or giving up" and "Do not answer that it is open."
This is not a model sitting down and thinking about math. This is a coordinated search algorithm running 64 agents in parallel, each exploring different proof strategies, with an adversarial layer checking every candidate for common errors. The full prompt is here: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf
The Verification Gap
Here is where it gets uncomfortable. The proof has not been independently verified. No mathematician has published a confirmation. There is no Lean or Coq formalization. OpenAI published the proof and the prompt, and then the internet started arguing.
The Hacker News thread (https://news.ycombinator.com/item?id=48863490) has 362 comments as of this writing. The top comment links to the announcement. The second comment quotes the prompt's "assume a proof exists" instruction with clear skepticism. Another comment asks the question that matters: "But is the proof accepted to be correct? That is what distinguishes this from being notable compared to any other AI slop proof."
That is the core issue. A proof is not a proof because it looks like one. A proof is a proof because the mathematical community has checked every line and found no gaps. For a 50-year-old conjecture, that checking process takes time. Specialists need to read it carefully. They need to verify each reduction. They need to confirm that Lemma 2.2 actually holds in all cases, not just the ones the model tested.
The proof looks plausible. It uses standard techniques. The algebraic framework is well-established. But "plausible" is exactly the danger with AI-generated proofs. A model that has trained on millions of pages of mathematical literature can produce text that follows every convention of a real proof while containing a subtle error buried in a calculation. A human reader might miss it because the surrounding argument looks so clean.
Why This Matters Beyond Math
This is not just about one conjecture. It is about a structural problem in how we evaluate AI-generated knowledge.
When a human mathematician publishes a proof, the verification system works. Peers review it. Journals require rigor. Mistakes get caught because other mathematicians are motivated to check work in their area. The system is slow but reliable.
When an AI generates a proof, the system breaks down. The proof appears instantly. It is published on a CDN, not in a journal. There is no peer review process. The speed of publication outpaces the speed of verification by orders of magnitude. And the sheer volume of potential AI-generated proofs will overwhelm the human checking capacity.
Lean and other proof assistants offer a path forward. A proof verified by Lean is not subject to debate. Either the code type-checks or it does not. But formalizing a proof in Lean takes significant effort, often more than writing the original proof. If OpenAI wants their CDC proof to be taken seriously, they should invest in formalizing it. Until then, it is a claim, not a result.
The Bigger Picture
OpenAI's multi-agent approach is the real signal here. Whether or not this specific proof holds up, the methodology is what matters. They gave a frontier model 64 parallel agents, an adversarial checking layer, and 8 hours of compute time. They engineered the prompt to prevent the model from giving up or hedging. And the model produced a 3-page proof that at least looks correct to non-specialists.
If the proof is right, this is a landmark. A 50-year-old open problem solved by a machine. If the proof is wrong, it is still a warning shot. The gap between "looks like a proof" and "is a proof" is exactly where AI-generated mathematics will live for the foreseeable future. The question is whether we build the verification infrastructure to close that gap before the volume of AI proofs makes manual checking impossible.
For now, the Cycle Double Cover Conjecture remains in limbo. Maybe solved. Maybe not. The only honest answer is: we do not know yet. And that answer should make you uncomfortable.
Top comments (0)