On July 10th, OpenAI published a three-page PDF claiming a proof of the Cycle Double Cover Conjecture — a problem that has been open for roughly fifty years — and attributed the proof entirely to GPT-5.6 Sol Ultra: sixty-four subagents, under an hour. The announcement traveled the way these things travel. By the time it reached my feeds it had already been compressed to AI solves yet another unsolved problem.
The Erdős page on this site has exactly one thesis: the dangerous moment in AI-assisted mathematics is not the idea — it is the promotion of an attractive answer into a trusted result. I wrote that sentence before this week. This week it came due. A claim like this is precisely the moment a verification project exists for, so instead of retweeting or scoffing, we graded it.
The conjecture, in plain words
Take any network of nodes and links, with one rule: no link is a lifeline. (A lifeline — a bridge, in graph theory — is a link whose removal splits the network in two.) The conjecture says you can always find a collection of round-trip loops through the network so that every link is traced by exactly two loops. Not one, not three — two, for every link, no matter how gnarly the network. Posed in the 1970s by Szekeres and Seymour (with roots in Tutte), it has resisted proof for five decades — and it has eaten claimed proofs before. At least two have appeared over the years and not survived scrutiny. That base rate matters, and it belongs in the same paragraph as the excitement.
What grading honestly means
I can't referee a general theorem from an armchair, and neither can any tool I run. What I can do is bound the claim with evidence — the same discipline the lab applies to its own work, aimed for the first time at someone else's. Four moves: pin the artifact, read it, execute what's executable, and kernel-check what a proof assistant can actually check. Then write down a verdict no larger than what those four moves establish.
Pin
A claim is a file, so name the bytes. The artifact is a three-page LaTeX PDF on OpenAI's CDN, no named human author, SHA-256 b4797f50…60fc13. No arXiv posting, no journal, no referee report, and no formal-verification artifact accompanies it. Everything below is about that exact file.
Read — and a confession
The argument is startlingly elementary. It leans on one genuinely classical result — the 8-flow theorem, settled in the 1970s — then does everything else with a local gluing trick and undergraduate linear algebra. I traced every step, both lemmas and the duality argument at the core, and found no error.
Here is the confession: that reading was done by the AI I work with, and the only other public line-by-line check I could find — posted in a Hacker News thread — was done by a model from the same family. Two careful reads that share a lineage are not two independent verifications. They are the same telescope pointed twice. I'm counting them as one lens, and saying so out loud, because silently counting them as two is exactly the kind of promotion this page exists to refuse.
Execute
The proof has one underrated property: it's a recipe. On any concrete network it says — find a certain labeling of the links, solve a certain small system of equations (which the paper's Lemma 2.2 asserts is always solvable), and read the loops off the solution. Recipes can be run. So we ran it, literally, with an independent checker on the output that trusts nothing from the construction.
409 out of 409 graphs produced verified cycle double covers. That includes the Petersen graph and four flower snarks — snarks are the danger zone here, because a minimal counterexample to the conjecture, if one exists, is known to hide among them — plus four hundred randomized networks, 139 of them with parallel links. The lemma the whole proof balances on held every single time. A network with a lifeline (which the theorem doesn't cover) was correctly refused rather than quietly mishandled, and the checker itself is tested to make sure it actually rejects corrupted covers. A checker that can't fail is a scoreboard, not an instrument.
Kernel receipts
Then we pushed two of those runs through the sternest gate in the lab: the outputs for the Petersen graph and the first flower snark were re-verified inside the Lean 4 proof assistant — kernel evaluation, zero axioms, the same empty-axiom standard as the lab's first verified node. Scope, stated as plainly as I can: those receipts certify the construction's outputs on two finite graphs. They do not certify the conjecture, and they do not certify the paper. Formalizing the general proof is a months-scale project and remains the gold standard this grade explicitly reserves space for.
The grade
| Question | Verdict |
|---|---|
| The artifact exists, is pinned, and states the real conjecture — including the fine print that sank earlier attempts | PASS |
| A careful line-by-line read finds an error | NO ERROR FOUND (one correlated lens) |
| The construction works when executed — 409/409, snarks included, falsifiable checker | PASS |
| Finite outputs kernel-checked in Lean, zero axioms | PASS |
| Peer review, independent expert verification, or a formal proof of the general theorem | NOT ESTABLISHED |
So the honest grade is: mechanically corroborated — not promoted. No lemma is false on any instance we could construct, the argument survives careful reading, and the theorem is still not established, because established means referees or a statement-audited formal proof, and neither exists yet. Two things would flip this grade overnight: acceptance by the graph theory community, or a Lean formalization of the general argument whose theorem statement is audited to match the conjecture. One thing would flip it the other way: a single graph where the paper's system has no solution. Our probe is the standing trap for that — any red run is front-page news in this journal.
I hope it holds. I want to live in the world where a machine found a three-page door into a fifty-year-old room, and if the referees agree, this entry becomes the record of the day we checked and it was real. Either way, the lane is the point: when the next proof-shaped object drops — and there will be a next one — the grading loop you just read ran start to finish in under a day, on one desk, in public. Trust the receipt. Then try to break it.