AI systems continue to accelerate at finding solutions to math problems.
OpenAI’s Ethan Knight posted on X that GPT-5.6 Sol Ultra, made generally available just a day earlier, had produced a proof of the Cycle Double Cover Conjecture, a graph theory problem that has sat unresolved since it was independently posed by George Szekeres in 1973 and Paul Seymour in 1979. The company published both the proof and the full prompt that generated it, and Knight capped off the post with an invitation for the community to dig in: “We’re excited to see what you all do with Ultra!”
The conjecture itself is easy to state and hard to prove. It asks whether every bridgeless graph, meaning one where removing a single edge never splits it into two pieces, has a “cycle double cover”: a set of cycles that together cover each edge of the graph exactly twice. Mathematicians have chipped away at special cases for decades. It holds for planar graphs, for 3-edge-colourable cubic graphs, and for graphs without a Petersen subdivision, among other partial results, but the general case has resisted a full resolution long enough that Open Problem Garden lists it as one of the most important open problems in graph theory.
The proof document credits the mathematics entirely to GPT-5.6 Sol Ultra, with Codex assisting on the writeup alongside a standard version of the model. The approach reduces the conjecture to cubic graphs, leans on the 8-flow theorem, and constructs a labeling of edges that forces each edge into exactly two cycles once a linear algebra argument is worked through. It’s dense, but it reads like a paper aiming for a journal rather than a press release.
What’s more unusual than the math is the process behind it, which OpenAI also disclosed in full. The prompt instructs the model to run up to 64 concurrent subagents and manage them “aggressively and dynamically,” rather than assigning fixed roles. Early rounds are meant to stay diverse, with agents pursuing different formulations, algebraic angles, and structural inductions independently, so the search doesn’t collapse onto one attractive but incomplete idea too early. Agents that hit a wall get marked as blocked and are only revisited if someone proposes a genuinely new mechanism. Adversarial agents are told to specifically hunt for edge cases: repeated-edge trails pretending to be cycles, disconnected graphs, cutvertices, and circular reasoning that smuggles in an unproven equivalent of the conjecture itself.
The prompt is also explicit that partial results don’t count. It rules out proofs restricted to special graph classes, constructions that cover most but not all edges correctly, reductions to other unproven conjectures, and computational verification up to some fixed size. It tells the model to spend at least eight hours before even considering giving up, and to return only when a complete proof survives its own internal audit. According to OpenAI, the whole run wrapped in under an hour.
The announcement landed on the Hacker News front page within its first hour and has already found its way into the Wikipedia entry for the conjecture, which now notes OpenAI’s claim dated July 10, 2026. That speed of uptake says something about how much attention frontier labs’ mathematical claims now draw, but it also means the proof is being read in public, by working mathematicians, before any formal peer review has happened. Coverage elsewhere has been careful to frame it as a claim rather than a settled result, and for good reason: the Cycle Double Cover Conjecture has attracted multiple previous “proofs” over the years, including several posted to arXiv, that were later found to have gaps or were withdrawn.
The release comes days after OpenAI rolled out the GPT-5.6 family more broadly, with Sol positioned against Anthropic’s Mythos-tier models on agentic and coding benchmarks, and just after the company made GPT-5.6 Sol generally available to ChatGPT users alongside a new business-focused product. A math proof of this stature, attributed directly to the model rather than to researchers using it as a tool, adds a different kind of headline to that run, one aimed less at developers comparing benchmark charts and more at mathematicians who’ve watched this specific problem sit open for half a century.
Whether the proof holds will now depend on people outside OpenAI working through all of it, line by line, the way any claimed resolution to a fifty-year-old conjecture has to be checked. If it stands, it will be a genuine landmark for what these systems can do unsupervised. If a gap turns up in Lemma 2.2 or anywhere else in the argument, it joins a long list of near-misses on the same problem, only this time with an AI’s name on the byline.