Breakthrough Tracker record
A formally verified proof package for the Cycle Double Cover Conjecture
The proof package establishes that every finite loopless bridgeless undirected multigraph has a multiset of cycles covering every edge exactly twice. A Lean formalization and two independent specialist expositions are public.
← Back to the filtered Breakthrough Tracker
- Stable ID
math-cycle-double-cover-2026- Revision
math-cycle-double-cover-2026.v1- Field
- Mathematics · Graph theory
- Evidence
- Tier 1 · Peer reviewed: No
- Record state
- Current · Formally verified claimed proof; strongly expert-supported
- Last checked
AI role
The originating package credits GPT-5.6 Sol Ultra for proof generation and Codex for assistance with the write-up.
Record details
- Problem or result
- Cycle Double Cover Conjecture
- Authors
- OpenAI proof system; independent expositions by Jim Geelen and Sang-il Oum
- Institutions
- OpenAI; University of Waterloo; Institute for Basic Science
- Result date
- Announced July 9–10, 2026; expert expositions July 16–17, 2026
Why it matters
The Szekeres–Seymour conjecture is a foundational, decades-old problem in graph theory and a prominent test of AI-generated research mathematics.
Limits
No peer-reviewed journal publication was located. Formal verification checks the encoded theorem and proof, while specialists must still assess exact correspondence with the accepted conjecture and the surrounding mathematical exposition.
Sources
- Primary: OpenAI proof PDF
- Primary: Original problem prompt
- Primary: Lean formalization repository
- Independent: Jim Geelen, OpenAI's proof of the Cycle Double Cover Theorem
- Independent: Sang-il Oum, An exposition of OpenAI's proof
- Independent: IBS seminar by Sang-il Oum
- Independent: Wolfram MathWorld status summary
Correction and revision history
- Added on 2026-07-22 with formal-verification and independent-exposition signals, while retaining a non-peer-reviewed status.
Machine-readable: JSON v1 · CSV v1 · Schema v1
This individual record remains noindex until a story-specific featured image passes Kingy’s rendered-pixel visual review. The source-linked tracker hub remains the public index.