The headline
On July 18, OpenAI published a three-page PDF titled A Proof of the Cycle Double Cover Conjecture, attributed to GPT-5.6 Sol Ultra. The Cycle Double Cover Conjecture is a genuinely hard, genuinely open problem in graph theory — every bridgeless graph has a set of cycles that covers each edge exactly twice, allegedly, and nobody's proven it since it was posed in the 1970s.
The story that spread: an AI cracked a 50-year-old problem in under an hour using 64 parallel subagents. It hit #1 on Hacker News with 559 points and 357 comments in a day. Ethan Mollick quote-tweeted it. Greg Brockman quote-tweeted it. The vibe was "AGI just did math nobody else could do."
That's not what happened. And the actual story — the one buried in OpenAI's own 10-page released prompt — is more interesting and considerably less magical.
What's actually in the prompt
OpenAI did something unusual and, credit where due, honest: they published the prompt that produced the proof. Read it and the "AI did math" framing falls apart fast.
The author — a domain expert who'd been working this specific problem with GPT-4/5.5 for about a year — didn't type "prove the Cycle Double Cover Conjecture" into a text box. The prompt is ten pages of scaffolding: known partial results, the specific proof strategies worth pursuing, the ones that are dead ends and why, notation conventions, and — this is the part that should be the headline — an instruction to assume a proof exists and work backward from that assumption, a known technique for getting language models to commit to a proof structure instead of hedging.
Then GPT-5.6 Sol Ultra ran 64 parallel rollouts (OpenAI's "test-time compute" branding for "we sampled it a lot and picked the one that didn't fall apart") and one of them produced a proof that survived a first read.
That's not nothing. That's also not "the model discovered a 50-year-old result on its own." It's a domain expert who already had the shape of the answer in his head, using a very good, very patient research assistant to fill in a search space he'd already mapped. One HN commenter nailed the analogy: it's like telling a contractor exactly which walls to knock down, which materials to use, and where the studs are, then crediting the contractor with designing the building.
The part everyone skipped: it's not verified
As of this writing, the proof hasn't been peer-reviewed. It's not machine-checked either — unlike DeepMind's AlphaProof, which only produces proofs formalized in Lean (meaning a proof assistant mechanically verifies every step), GPT-5.6's proof is natural language. A human has to read it and vouch for it, the same as any human-written proof submitted to a journal.
Mathematician Thomas Bloom, one of the first people with the expertise to actually evaluate it, called it "very nice" and "elementary" — and noted it plausibly could have been found in the 1980s with existing techniques. He also flagged something less flattering: the proof doesn't cite foundational prior work, including a 1983 paper by Bermond, Jackson, and Jaeger that's directly relevant. That's not a minor style nit in a math proof — citation gaps are often where you find out an argument silently depends on a case someone already knows is broken.
So the current state of the art, three days later, is: promising, elementary by expert standards, missing citations to work it may be leaning on, unverified. Ship first, verify later — sound familiar?
Why this is happening now
Zoom out and the timing makes sense. GPT-5.6 went GA on July 9 as a three-tier family — Sol ($5/$30 per million tokens), Terra ($2.50/$15), Luna ($1/$6) — undercutting Anthropic and Google on price while claiming the top spot on Terminal-Bench 2.1 (91.9% for Sol Ultra vs. 88.0% for Claude Fable 5). A splashy, hard-to-verify-quickly math result dropped nine days into general availability, framed as an "AGI moment," is a marketing move, not a research paper. Papers get submitted to venues. This got a CDN link and an X thread.
Worth noting: on SWE-Bench Pro — a harder, more production-realistic coding benchmark than Terminal-Bench — Claude Fable 5 scores 80.0% against Sol's 64.6%. OpenAI led with the benchmark it wins and the mathematically photogenic headline. That's not a criticism of the model. It's a criticism of reading launch-week benchmark selection as ground truth.
What to actually take from this
- The tool is real. A model that can hold ten pages of expert-supplied context, run 64 parallel proof attempts, and produce something a working mathematician calls "very nice" is a legitimately useful research tool. If you do formal methods, theorem proving, or search-heavy technical work, GPT-5.6 Sol Ultra is worth your API budget to try.
- "AI solved it" and "AI helped an expert who already knew the shape of the solution finish it faster" are different claims, and headlines collapse them on purpose because the second one doesn't trend.
- Unverified is not synonymous with wrong, but it's also not synonymous with right. Wait for the citation gaps to get resolved and for someone besides the vendor's own CDN to confirm it before you cite "GPT-5.6 proved a 50-year-old conjecture" as a fact in your next deck.
- The prompt-engineering story here is the actually reusable part. "Assume a proof exists, work backward" is a general technique for getting reasoning models unstuck. That's the artifact worth stealing from this release — not the conjecture.
The pattern to watch for, every time one of these drops: check whether the vendor published the prompt. If they did and it's ten pages of expert scaffolding, you're looking at a very good autocomplete for a human who already knew where they were going. If they didn't publish it, ask why.
Sources: OpenAI's proof PDF, the released prompt, HN discussion, GPT-5.6 Sol launch details.
Top comments (0)