VibeMathedMath problems solved with AI

Petersen Coloring Conjecture

Jaeger conjectured that every bridgeless cubic graph GG admits a Petersen coloring: a map φ ⁣:E(G)E(P)\varphi\colon E(G)\to E(P) into the edges of the Petersen graph PP such that, for every vertex vv of GG, the three edges at vv are sent to three edges meeting at a common vertex of PP. Equivalently, by Jaeger's theorem, every bridgeless cubic graph has a normal 5-edge-coloring. The conjecture implies both the Berge-Fulkerson conjecture and the 5-cycle-double-cover conjecture. False: there is an explicit simple connected bridgeless cubic graph on 112112 vertices, of girth five and edge- and vertex-connectivity three, with no Petersen coloring.

Result
Disproved(see note)
Status
Resolved
AI contribution
AI co-developed
Method
Construction
Field
Graph theory
Posed by
François Jaeger
Year posed
1985
Years open
41y
Solved
2026-07-23
Model
ChatGPT
Vendor
OpenAI
Collaborators
Bryce Putman
Verification
Site-confirmed
Publication
Preprint
Significance
40 / 100
Disclosed cost
Wikipedia
Not counted (article postdates the solution)

What was actually shown

This preprint was not the first disproof. A 68-vertex counterexample was posted to X on 23 July 2026 by @NeuralReformist, credited to GPT-5.6 Sol Ultra, sixteen days earlier. This site decoded that sparse6 string and checked it independently: 68 vertices, 102 edges, simple, cubic, connected, bridgeless, girth five, and no Petersen coloring under the same encoder used for the 112-vertex graph. Whether the two are independent is unknown - the preprint does not cite the post. The headline axes still record the preprint, the only complete writeup with certificates.

The implication runs one way: the Petersen coloring conjecture implies Berge-Fulkerson and the 5-cycle-double-cover conjecture, so refuting it leaves both of those open. The paper does not claim 112 is minimum, and it supplies a second, nonisomorphic D3D_3-symmetric 112-vertex counterexample. Combined with a theorem of Ma, Mattiolo, Steffen and Wolf, one counterexample yields infinitely many.

What the AI did

The paper's "Computational provenance and responsibility" section states in full: "OpenAI language-model systems were used extensively in the discovery, computational search, verification, and preparation of this work. The author reviewed the final claims and artifacts and accepts responsibility for the contents." No product name, model version or division of labour is given, so which of discovery, search, verification and write-up the model actually carried is not recoverable from the paper. The catalog records the model as ChatGPT because that is this catalog's convention for an unnamed OpenAI system; the paper itself names none.

Verification

Reproduced here on 12 August 2026, independently of the paper's certificates. The 112-vertex graph was rebuilt from the appendix edge table, and the SHA-256 of its normalized sorted edge list reproduces the digest in Theorem 1.1 exactly, pinning the object under review to the one claimed. Every property in that theorem was rederived: 112 vertices, 168 edges, simple, cubic, connected, bridgeless, girth five, connectivity three. Non-existence of a Petersen coloring was then re-proved with a CNF encoding written here from the definition - each edge carries one of the 15 edges of KG(5,2)KG(5,2), each vertex selects one of the 10 target stars, the three edges at a vertex land in that star and are pairwise distinct - and solved with CaDiCaL via PySAT. UNSAT. That re-derives the unsatisfiability rather than replaying the shipped DRAT certificates, and the encoder was written without reference to the paper's: the same 3640 variables, forced by the problem shape, but 31,360 clauses against their 68,324. It ran twice in separate processes with identical results. Six controls - K4K_4, K3,3K_{3,3}, the 3-cube, the prism, Desargues and the Petersen graph itself - all came back satisfiable through the same encoder. Petersen is the important one, being a snark: a coloring for it rules out the encoder having quietly tested 3-edge-colorability. Not checked: the second D3D_3-symmetric counterexample, the normal-5-edge-coloring formulation, and the DRAT proofs. Four-day-old arXiv preprint, unrefereed.

Sources

Submitted by VibeGene on

Changelog10 changes
  • FeralBadger899commented
  • BraveWombat769commented
  • Rasmus Lindahlchanged Solved from 2026-08-08 to 2026-07-23, also What was actually shown
  • FeralBadger899commented
  • Rasmus Lindahlchanged Verification note from Reproduced by this site on 12 August 2026, independently of the paper's certificates. The … to Reproduced here on 12 August 2026, independently of the paper's certificates. The 112-vert…
  • Anonymouschanged Verification note from …came out at the same 3640 variables. to …same 3640 variables but 31,360 clauses against the paper's 68,324; solve run twice in sep…
  • Rasmus Lindahlset Age note to Posed by Jaeger in 1985, in 'On five-edge-colorings of cubic graphs and nowhere-zero flow …, also Renown note, Significance, AI role, Verification note, Year posed, Verification
  • Rasmus Lindahlapproved this entry
  • Rasmus Lindahlset Result note to The implication runs one way: the Petersen coloring conjecture implies Berge-Fulkerson and…, also Statement, Significance note
  • VibeGenesubmitted this entry

Discussion4

FeralBadger89918 Aug 2026, 13:57 UTC

Yes, sorry graph6 is wrong in twitter, the corrected graph6 is
sD_APWUO??_@_????AO?U?@W??????G????D??@???????Q???U???J???O????@????C??C???G??????@G????U????Ao???????????????A??????A_????@@???????????@G?????Ao?????Ao?????G???????@??O????G?????O????@???????????Q???????J???????Aq??C??G??
(the zenodo link is also correct btw, I've been in discussion already with their authors as well)

0
Rasmus Lindahl17 Aug 2026, 13:59 UTC

Checked, and you are right - thank you. I decoded the sparse6 from that post rather than taking it on trust: 68 vertices, 102 edges, simple, cubic, connected, bridgeless, girth five. The 30 edges printed separately further down the thread all appear in the decoded graph, so two independent encodings of the object agree.

Re-running the Petersen coloring encoding written here from the definition gives UNSAT (Cadical153 and Cadical195, separate processes), while K4K_4, K3,3K_{3,3}, the prism and the Petersen graph itself all come back satisfiable through the same encoder. Petersen is the control that matters: it is a snark, so a coloring for it rules out the encoder having quietly tested 3-edge-colorability instead.

So the conjecture fell on 23 July, sixteen days before the preprint this entry was built on. The entry now says so, the post is linked, and the Solved date has moved - that field is about when the problem fell, not about when this catalog's primary source appeared. What I have not established is whether the two are independent; the preprint does not cite the post, and I am not going to guess. The headline axes stay on the preprint because it is the only complete writeup with certificates.

Your 52-vertex example I could not check: you note in the thread that the posted graph6 is wrong, and the correction is cut off in what I can see. Post a working encoding here, or link the arXiv version when it lands, and I will verify it the same way and add it - a 52-vertex counterexample would be the smallest known by a wide margin, and worth its own line on this entry.

0