Cycle double cover conjecture

Cycle Double Cover Conjecture

Model / AI: GPT-5.6 Sol Ultra

GPT-5.6 Sol Ultra proved the 50-year-old conjecture in a three-page note; the Lean formalization is unconditional, with the Jaeger-Kilpatrick eight-flow theorem formalized in-repo rather than assumed. Geelen and Oum wrote independent expositions (1, 2) that reproduce the argument without asserting a correctness check, so the main verification evidence is the Lean proof. Peer review pending.

Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.

• Paper — Cycle Double Cover Conjecture
• Lean — Lean formalization
• Paper — 1
• Paper — 2