OpenAI has published a three-page manuscript that claims to prove the Cycle Double Cover Conjecture, a graph-theory problem that has resisted a generally accepted proof since the 1970s.
The document states that the proof is entirely due to GPT-5.6 Sol Ultra and that Codex with GPT-5.6 Sol assisted with the write-up. A public account of the run says the Ultra system used 64 cooperating subagents and completed its search in under an hour.
The manuscript is real and available for anyone to inspect. The theorem is not yet settled merely because the PDF exists. The right headline is that OpenAI has released a candidate proof under active review.
What the conjecture says
A graph contains vertices connected by edges. A bridge is an edge whose removal disconnects part of the graph. The Cycle Double Cover Conjecture asks whether every finite bridgeless graph has a collection of cycles such that every edge appears in exactly two cycles, counting multiplicity.
The word “exactly” carries the difficulty. It is not enough to find many cycles or cover every edge at least once. The cycles must be coordinated so no edge is missed or overused.
The problem is associated with independent formulations by George Szekeres, Paul Seymour, Itai and Rodeh, and William Tutte in the 1970s and 1980s. Many special cases and related flow results are known, but claimed general proofs have historically failed to gain acceptance.
The proposed route
The OpenAI manuscript says it reduces the problem to loopless cubic graphs, where every vertex has degree three. It then uses a nowhere-zero flow over the group
Gamma = F_3^2The paper connects this labeling to the 8-flow theorem and attempts to convert each edge label into a two-element set. At every vertex, each group element should then occur either zero times or twice among the incident edge sets.
If that local property holds, the edges associated with each group element form cycles. Since each edge receives two elements, each edge is included twice across the resulting cycle collection.
The manuscript’s key work is the conversion from the flow labeling to those paired edge sets. It says the final reduction becomes an elementary linear-algebra argument.
That is an appealing proof shape: established reduction, established flow theorem, a new labeling lemma, and a short construction. It is also exactly where reviewers should concentrate.
Why a three-page proof can be plausible and dangerous
Short proofs of old problems do happen. A long history of partial results can make the final argument compact because it builds on strong existing machinery.
Shortness also makes omitted conditions dangerous. Reviewers will need to check:
- Whether every cited reduction applies to multigraphs under the paper’s definitions.
- Whether orientation choices preserve the required flow properties.
- Whether the edge-set construction works for every local configuration.
- Whether the linear-algebra step guarantees global compatibility.
- Whether parallel edges and length-two cycles are handled consistently.
- Whether any lemma silently assumes 3-edge-colorability, excluding the difficult snark cases.
One invalid transition can collapse the conclusion even when the overall idea looks elegant.
What 64 subagents may have contributed
OpenAI describes Sol Ultra as a mode that coordinates multiple agents for difficult work. The company’s general GPT-5.6 release says Ultra coordinates four agents by default, while accounts of this specific experiment describe a larger 64-agent run.
For mathematics, parallel agents can explore different proof routes, attack lemmas, search for counterexamples, and critique one another. The synthesis step remains critical. Sixty-four plausible fragments do not automatically form one valid proof.
The public prompt and run details are therefore scientifically important. They can show how much mathematical scaffolding came from the operator, what references were supplied, and whether another team can reproduce the route.
Verification should happen at three levels
Specialist review: Graph theorists should check the argument against the existing literature and known failure modes of earlier proof claims.
Independent reconstruction: A reviewer should be able to rebuild the result from the definitions without relying on the model’s prose.
Formalization: Lean, Coq, or another proof assistant could eventually verify the finite algebraic core, although formalization is substantial work and does not replace checking that the formal theorem matches the original conjecture.
Until those stages advance, the proof should be discussed as a manuscript, not as a certified resolution.
The signal
This release is still consequential even before a verdict. OpenAI did not publish only a benchmark score; it published a compact mathematical object that experts can attack line by line.
If the proof survives, it will be a major result for graph theory and AI-assisted research. If a gap is found, the experiment will still reveal whether multi-agent systems can generate promising research programs and how quickly expert feedback can refine them.
The productive standard is not “Did the AI sound convincing?” It is “Did the argument create a new result that independent mathematicians can verify?”
