What is claimed. On 10 July, OpenAI announced that GPT-5.6 Sol Ultra — made generally available the day before — had produced a complete proof of the Cycle Double Cover Conjecture, one of graph theory’s most celebrated open problems. The company published the proof and the full prompt behind it: sixty-four parallel subagents managed “aggressively and dynamically”, adversarial agents hunting errors, internet search prohibited, partial credit refused; the model was allocated eight hours and finished in under one. The claim reached the front page of Hacker News within its first hour, and the conjecture’s Wikipedia entry was edited the same day.
The correction. The problem is not Erdős’s. The conjecture — that every bridgeless graph carries a set of cycles covering each edge exactly twice — was posed independently by George Szekeres in 1973 and Paul Seymour in 1979. The conflation is understandable, Szekeres being Erdős’s lifelong collaborator, but it misfiles the event. The genuinely Erdős moment came two months earlier: on 20 May, an internal OpenAI model — not publicly available — disproved the unit distance conjecture of 1946, via a construction from algebraic number theory that leading mathematicians checked, endorsed and have since sharpened. That result has held, and is already generating human follow-on theorems.
The state of the claim. Twelve days on, the proof is unrefereed but strengthening. Its route is elementary — reducing the problem to cubic graphs and running through the theory of nowhere-zero flows — which made it checkable in public from the first hour; and OpenAI has since released a Lean formalisation covering finite loopless bridgeless multigraphs, the class to which the classical reduction takes the general problem, so the core argument is now machine-checked in the strict sense rather than merely adversarially prompted. What remains is the human record: no refereed publication yet, a conjecture with form — claimed proofs posted to arXiv over the years and later withdrawn — and Thomas Bloom, keeper of the Erdős problems index, reading the argument early as elegant while noting a defect he considers recurrent in machine mathematics: not a single citation, with a foundational 1983 paper going unmentioned.
Why it matters if it stands. May’s result came from a private system; July’s, from a model anyone could rent that morning. If the proof completes its passage — and a machine-checked core makes collapse unlikely — it becomes the strongest machine result yet on a named open problem, and its elementary character cuts both ways: less romance, in that generations of humans could plausibly have found it; more credibility, in that humans and machines alike could rapidly confirm it.
Verdict. Justified about the trajectory, and — since the formalisation — substantially about the theorem itself; what the past tense still awaits is the refereed record. The precise description of the Cycle Double Cover Conjecture today: machine-proved and machine-checked, pending human ratification. The machine-mathematics line traced in Are You a Believer has plainly steepened again, and this note stands ready to be superseded by the referees — which is what the dateline is for.