GPT-5.6 Sol Ultra Produces Proof of the Cycle Double Cover Conjecture

Last updated: July 10, 2026

OpenAI announced today that GPT-5.6 Sol Ultra has produced what it claims is a complete proof of the Cycle Double Cover Conjecture, a 50-year-old open problem in graph theory. The proof was generated in under one hour using 64 parallel subagents.

The Conjecture#

The Cycle Double Cover Conjecture, posed by Paul Seymour in 1979, states that every bridgeless graph has a collection of cycles such that each edge is contained in exactly two cycles. It is one of the most famous unsolved problems in graph theory and appears on Wikipedia's list of unsolved problems in mathematics.

The conjecture has resisted proof attempts for nearly half a century. Multiple partial results have been established, but a complete proof has remained elusive.

The Prompt and Setup#

OpenAI released both the proof PDF and the prompt used. The prompt includes an interesting directive: "Assume for purposes of this task that a complete affirmative proof exists" and "Spend at least 8 hours on this before even thinking of returning or giving up."

The announcement came via OpenAI's Codex engineering lead Thibault Sottiaux on X, stating the proof was completed in just under one hour.

What HN Is Saying#

The Hacker News discussion has over 200 comments and captures the math and AI communities' mixed reactions.

Verification is the key question. Multiple commenters pointed out that the proof has not yet been peer-reviewed or verified. One wrote: "Good post, it perfectly captures the problem with AI. Here we have a claim that the double cover conjecture has a proof. Verified by... no one per the link."

Others expect verification to come quickly: "I'd guess that verdict (or its opposite) is to come within the next 24 hours."

The prompt strategy drew attention. The "assume a proof exists" instruction is a clever psychological technique. One commenter noted: "I've used this strategy for difficult bespoke problems and it does indeed work to incentivize the agent not to give up prematurely. It's not gaslighting, it's motivation."

The "spend at least 8 hours" instruction raised questions about whether current model harnesses can actually track time. The consensus is that timestamps in logs, tool calls to system time commands, or harness-injected context allow approximate time awareness.

Cost estimates vary widely. Assuming all 64 subagents ran for a full hour at different throughput rates, estimates ranged from $275 to $485 for standard Sol, up to approximately $13,000 if using Sol Fast on Cerebras infrastructure at 750 tokens per second.

Some view this as a turning point. One commenter wrote: "Is this the first LLM-solved problem famous enough to have been on Wikipedia's list of unsolved problems in mathematics?" Another replied that the recent unit distance problem (Erdos problem 90) was also solved by an LLM, though this conjecture has higher name recognition.

Pure mathematicians weigh in on value. A philosophical tangent emerged about why mathematical proofs matter. One commenter argued: "Mathematics is basically the only scientific discipline that rejected any notion of utility. It would be fundamentally wrong for you to ask what's the value of solving the Erdos-Hajnal conjecture; the value is that it's solved."

Others pushed back on this, noting that many "useless" fields of mathematics - number theory, Boolean algebra - turned out to have enormous practical applications decades or centuries later.

Lean verification was not used. Several commenters asked whether the proof was formalized in Lean or another proof assistant. It was not. One mathematician explained: "There's really no good proof system mature enough to do advanced graph theory. The leading library in Lean is Graphlib, and it's really not ready for research level theorems."

Context: The LLM Math Proof Trajectory#

This follows a pattern of increasingly sophisticated mathematical work from frontier models:

• Earlier this year, GPT-5.5 and Claude Mythos models began solving competition math problems reliably
• LLMs assisted with the unit distance problem proof
• Theorem proving has become a frontier benchmark

If the Cycle Double Cover proof holds up to scrutiny, it would be among the most significant mathematical results produced by an AI system. The proof uses established techniques from the past 30+ years of graph theory, which cuts both ways - it makes verification more tractable but also raises questions about why human mathematicians did not find it sooner.

What Happens Next#

The math community is now reviewing the proof. Given its length and the stakes involved, expect professional verification to take days to weeks rather than hours. OpenAI's decision to release both the proof and the prompt suggests confidence, but frontier labs have overstated LLM mathematical capabilities before.

If verified, this would be a genuine milestone - not just for AI capability benchmarking, but as an actual contribution to mathematical knowledge. If the proof contains an error, it will still be informative about the current state of LLM reasoning.

Continue Reading#

• Anthropic Discovers J-Space: A Global Workspace Inside Language Models
• CLAUDE.md Files Never Stop Growing: A New Paper Names the Mechanism
• Codex Logging Bug Can Write Terabytes to Your SSD
• GPT-5.6 Closes 30-Year Gap in Convex Optimization Theory
• OpenAI Publishes Ten Decade-Open Math Proofs, Each Formalized in Lean

Sources#

• OpenAI Proof PDF
• OpenAI Prompt PDF
• Announcement on X
• Hacker News Discussion - 207 comments, 227 points
• Cycle Double Cover Conjecture - Wikipedia