OpenAI has announced that its new AI model, GPT-5.6 Sol Ultra, has generated a complete proof of the Cycle Double Cover Conjecture. The conjecture, which asks whether any network of vertices and edges contains a set of cycles that traverses each edge exactly twice, had remained unproven for about 50 years. The model completed the task in under an hour by using 64 subagents working in parallel.
The problem and the proof
The Cycle Double Cover Conjecture was formulated independently by several mathematicians in the 1970s. Over the decades, many partial solutions emerged for special cases, but no generally accepted proof existed until now. According to OpenAI, the proof comes entirely from GPT-5.6 Sol Ultra, and the paper was written by the model itself.
Mathematician Thomas Bloom of the University of Manchester reviewed the proof and called it "a very nice proof." He noted that the solution is "short, elementary, and could have been discovered in the 1980s." It does not require any new mathematical theories but cleverly combines known tools.
Bloom speculated on why human mathematicians did not find the proof earlier. He suggested the key step involved a small, counterintuitive twist in the reasoning. A human mathematician would likely try the obvious approach, see it fail, and move on. The AI does not get discouraged and keeps trying small variations until one clicks.
"One can imagine trying the natural labelling first, checking the linear algebra, and when that failed shrugging and thinking 'oh well, I was expecting to fail, guess it can't be done this easily' while the AI does not get discouraged and keeps trying small variations," Bloom wrote.
Bloom's assessment is the most detailed public evaluation so far. A full mathematical verification by the scientific community is still pending.
Citation concerns and AI's creative role
Bloom pointed out that the core mathematical ideas behind the proof trace back at least to a 1983 paper by Bermond, Jackson, and Jaeger. He criticized OpenAI's paper for not mentioning this prior work at all. Anyone reading only the paper might think the AI invented the underlying strategy itself.
"I assume that these previous works were a big influence on the OpenAI proof, and it is a shame that it does not mention them at all," Bloom wrote. "This is a frequent issue with AI-generated proofs and papers: they use ideas and proof strategies taken from the literature without proper citation."
The mathematician doubted the AI came up with the solution entirely on its own, "given that its first problem-solving instinct is generally to search for all related papers on a problem and read them."
Stay updated
Get the day's AI and automation news in your inbox. No spam, unsubscribe anytime.
This debate is a recurring theme around reasoning models. Do they merely find existing knowledge and recombine it? Or do they produce something new through creative work? For this proof, Bloom seems to lean toward the former.
What this means for open problems
Bloom compared the result to the unit distance conjecture, which OpenAI also recently solved. Both were major open problems "that turned out to be much easier than expected no big new theories were required, and one can imagine many alternate histories when these proofs were found decades ago," he wrote.
He expects AI systems to crack more conjectures like this, "those whose solutions require only existing, well-developed, theory, plus a lot of patience and belief." But according to Bloom, "this is likely only a small proportion of open problems, and we don't know in advance which they are."
"But in this strange new world where big AI companies are spending a lot of time and money attacking many open problems at once (and only reporting the successes, of course), we will soon find out more of what was within our reach all along," he wrote.
How the prompt drove the solution
Part of the solution lies in the prompt written by humans. It engineers exactly the kind of persistence Bloom described as key to finding the proof. First, the prompt tells the model to assume a complete proof exists, cutting off its most likely honest answer that the conjecture is open. Then it bans the model from searching the internet to check whether the conjecture has already been solved and from answering that the conjecture is unsolved. The model has nowhere to go except solving the problem.
Verification is just as strict. Partial results, reductions to other unproven conjectures, summaries of the current state of research, and explanations of why the problem is hard were all rejected as insufficient. The model cannot respond until a complete proof is ready and passes an adversarial test.
The rest of the prompt reads more like directives from a research lab than a typical AI prompt. Most of the 64 agents are deliberately kept in the dark about which approach currently looks most promising to encourage independent thinking. Adversarial agents then check each candidate proof against a detailed list of typical errors, looking for things like closed paths incorrectly identified as cycles or reductions that accidentally create new bridges in the graph.
The model was told to compute for at least eight hours before it could even consider giving up. It finished in one.