Cycle double cover conjecture proved for all bridgeless multigraphs
Every finite bridgeless loopless multigraph has a multiset of cycles covering each edge exactly twice, resolving a conjecture open since 1973, with a machine-checked Lean proof of the unconditional statement.
- Lab
- OpenAI
- Model
- GPT-5.6 Sol Ultra
- Field
- Mathematics
- Date
- 2026-07-10
- Problem posed
- 1973 · open 53 yrs
Sources
Original work
Announcement
Media coverage
Independent commentary
What was found
The cycle double cover conjecture, posed by Szekeres in 1973 and independently by Seymour in 1979, asks whether every bridgeless graph admits a multiset of cycles in which every edge appears exactly twice. It is a textbook open problem in graph theory and sits at the centre of a cluster of neighbouring conjectures. OpenAI announced on 10 July 2026 that GPT-5.6 Sol Ultra, running 64 concurrent subagents, produced a three-page proof of the full statement in under an hour, and published the proof and the prompt, with a Lean 4 formalization following. The formalized route goes through the Jaeger–Kilpatrick eight-flow theorem: it constructs a nowhere-zero flow valued in three copies of the integers mod two, then converts that flow into a cycle double cover. Sang-il Oum published a ten-page exposition a week later, presenting the argument with slight modifications intended to make it more accessible.
Novelty check
The conjecture is recorded as open in the standard references, including Wolfram MathWorld, and has a documented history of proof claims posted to arXiv that were later withdrawn or found to have gaps, so the prior state was unambiguously unresolved. One thing complicates the picture rather than the novelty: Shiva Kintali posted an independent Codex-assisted proof claim of the same statement three days later (arXiv:2607.14140), also routed through nowhere-zero three-bit flows and likewise unreviewed. The result is a new proof, not a retrieval of a known one.
Caveats and known objections
Not peer-reviewed. The conjecture's history of gapped proof claims is itself a reason for caution, and mathematicians are treating this one as unconfirmed pending expert review. The Lean development does check the unconditional statement for finite loopless bridgeless multigraphs, sorry-free and admit-free with no project-specific axioms, but it is first-party, produced by the same organisation as the proof, and had no independent audit at entry time. Autonomy graded ai-led rather than autonomous: the published prompt supplies more than the problem. It instructs the model to assume for purposes of the task that a complete affirmative proof exists, enumerates the approach families to explore including the flow formulations the proof in fact used, and specifies the 64-agent search strategy in detail.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Community discussion
Graded formally verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Cycle double cover conjecture proved for all bridgeless multigraphs. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-07-10-cycle-double-coverBibTeX
@misc{whataifound-openai-2026-cover,
title = {Cycle double cover conjecture proved for all bridgeless multigraphs},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-07-10-cycle-double-cover}
}