OpenAI says its GPT-5.6 Sol Ultra model produced a complete proof of the Cycle Double Cover Conjecture, a graph theory problem that had gone unsolved since it was independently posed by George Szekeres in 1973 and Paul Seymour in 1979. The company published the proof as a PDF on its own servers on July 10, and mathematicians outside OpenAI have since begun checking it line by line.
The conjecture asks whether every bridgeless graph — one with no edge whose removal would split it in two — can always be covered by a set of cycles that together pass over each edge exactly twice. It is considered a foundational open question in graph theory, one that has attracted and defeated multiple attempted proofs over five decades.
How the proof was produced
According to OpenAI, the model was set loose with a prompt instructing it to run up to 64 subagents concurrently and manage them “aggressively and dynamically.” Early on, the subagents were kept deliberately unaware of each other’s progress so they would pursue distinct angles — different algebraic formulations and structural inductions — rather than converging prematurely on one idea. Separate adversarial agents were tasked with hunting for errors against known failure patterns common in past attempted proofs. OpenAI says the full process, from prompt to finished write-up, took under an hour, though the model had been instructed to keep working for at least eight hours before giving up.
Mixed reception from mathematicians
Thomas Bloom, a mathematician at the University of Manchester, gave the proof its first substantive public review, calling it “a very nice proof” that is “short, elementary, and could have been discovered in the 1980s” using tools already available at the time. He credited the model for persisting through minor variations on an approach rather than abandoning it early, as a human researcher might.
Bloom was more critical of the write-up’s scholarship, noting it cites no prior work at all — including a foundational 1983 paper by Bermond, Jackson and Jaeger that laid out ideas the new proof builds on. He called the omission “a frequent issue with AI-generated proofs and papers,” which often reuse strategies from the literature without attribution.
Neither OpenAI nor outside reviewers have declared the proof formally verified: it has not been checked in a proof assistant such as Lean, and Bloom said a full community review — stress-testing each reduction against the general case — will likely take days to weeks. The conjecture has a history of drawing plausible-looking but ultimately flawed proofs, so mathematicians are treating the result as promising but provisional.