OpenAI released a three-page manuscript on July 10, 2026 that it says its GPT-5.6 Sol Ultra model generated to prove the Cycle Double Cover Conjecture, a graph-theory problem open for about 50 years. The claim is real and the artifacts are public, but no mathematician has yet verified the proof and there is no machine-checked version -- so the story is not "AI proved a theorem," it is "AI produced a plausible-looking proof that humans have not yet been able to check."
Key facts
- The headline number: OpenAI says the result came from 64 model instances working together as subagents, in just under one hour.
- When: Announced July 10, 2026; the Wikipedia page for the conjecture was updated the same day to note the preprint.
- Who: OpenAI, using GPT-5.6 Sol in "Ultra mode"; the final PDF was formatted by Codex.
- Primary source: OpenAI's proof manuscript and the Hacker News discussion.
Here is the background a non-expert needs. A graph is just dots (vertices) joined by lines (edges). "Bridgeless" means you cannot disconnect the graph by cutting a single line. The Cycle Double Cover Conjecture, credited to Tutte, Szekeres, and Seymour and open since the 1970s, asks a deceptively simple question: can you always find a set of loops (cycles) so that every line in the graph is walked over exactly twice, no more and no less? It sounds like a puzzle you could solve on a napkin, but it has resisted proof for half a century and connects to deep questions about the structure of networks.
What OpenAI actually released is a manuscript claiming that "every finite loopless bridgeless undirected multigraph has a cycle double cover," plus something unusual: the exact prompt used to steer the model. That prompt is the tell. It does not just ask the model to solve the problem; it spends most of its length forbidding the model from giving status reports, expressing vague optimism, or declaring intermediate steps "routine" -- in effect, ordering the model to keep grinding instead of bailing out. On Hacker News, the top comment (from user mNovak) captured the reaction: it is "interesting how much of the prompt, even in this latest-and-greatest model, is spent essentially telling the model to actually solve the problem."
How it works is the genuinely interesting part. Instead of asking one model for a single answer, OpenAI orchestrated 64 instances working in a loop -- proposing, checking, and discarding lines of attack. Think of it less as one genius and more as a room of 64 tireless graduate students who never get discouraged, coordinated by a strict supervisor who refuses to let anyone say "this looks hard, let us stop." This is the practical face of what people call System 2 reasoning: slow, deliberate, multi-step problem-solving built out of many cheap thinking steps rather than one big one. It is closely related to the ideas behind chain-of-thought reasoning and test-time compute -- spend more computation at answer time to think harder.
Why it matters: if the proof holds, it would be one of the first times an AI system settled a long-standing open problem in pure mathematics, not just reproduced a known result. And the mechanism -- orchestrated agents rather than a bigger single model -- would suggest that a lot of near-term capability gains will come from how models are looped and steered, not only from their raw weights.
Now the honest caveat, which is the whole story for mathematicians. A PDF is just text. A proof is only accepted when other experts can follow every step, or when it is written in a proof assistant like Lean or Coq that mechanically checks each inference. OpenAI released neither an expert endorsement nor a machine-checkable proof. On the rigor-focused communities -- r/mathematics, r/MachineLearning, r/LocalLLaMA -- the reaction is blunt: show us the Lean code. Several people flagged that three pages is suspiciously short for a 50-year-old conjecture, and that language models are known to produce proofs that mimic the structure of a valid argument while hiding a fatal logical gap -- the mathematical equivalent of a hallucination. On the more optimistic r/singularity, the excitement is less about this one theorem and more about the 64-subagent recipe as a preview of how agentic AI will tackle hard reasoning.
The so-what: treat this as a claim under review, not a settled result. The next real milestone is not another announcement -- it is a machine-checked proof, or a named mathematician putting their reputation behind it. Until one of those lands, the correct reading is that OpenAI has demonstrated an impressive, heavily-steered search process that produced a document no human has yet confirmed is correct.
Originally published on Ground Truth, where every claim is checked against the primary source.
Top comments (1)
Your framing that the open question is the missing machine-checked version is the right one, and it's worth being exact about why the 64-instance setup doesn't already answer it. Those 64 instances proposing and discarding attacks are all the same model. They share weights and a training distribution, so they share blind spots. A systematic error in some class of graph reasoning shows up in all 64 at once, and their mutual checking converges on it. So agreement across the 64 mostly measures how consistent the model is with itself. It counts one prior 64 times and reports the tally as confidence.
That's the real reason a Lean or Coq proof is the thing people are asking for. A formal checker shares none of the generator's assumptions, so its failure surface doesn't overlap with the model's. It can reject something the whole ensemble was certain of.
The prompt detail points the same way. A model you have to explicitly forbid from calling steps "routine" or bailing early is a model whose cheap self-checks are worth very little. You tuned it for persistence, and persistence is exactly the pressure that suppresses the "I'm not sure here" flag. That hesitation is the signal an outside verifier most wants to see.