In the news: an openAI prompt , an openAI proof of the Cycle Double Cover Conjecture , a Lean verification and a reddit discussion. Above, a graph is given a double cover.
MathWorld: Cycle Double Cover Conjecture.
So-- how do we check this? One start is to throw difficult graphs at it. And the hardest graphs are snarks. First... I asked OpenAI to build supporting code.

Supporting Code


Use the code

The simplest snark is the Petersen Graph. Lets see what the code does.
In[]:=
snarks=SortBy[GraphData["Snark"],GraphData[#,"VertexCount"]&];
In[]:=
snarks[[1]]
Out[]=
PetersenGraph
In[]:=
pete=cycleDoubleCoverData[GraphData[snarks[[1]]]]
Out[]=
{Edges{113,214,316,424,525,627,735,838,949,10510,1167,12610,1378,1489,15910},Flow{1{0,1,1},2{1,1,0},3{1,0,1},4{1,1,1},5{1,1,0},6{0,0,1},7{1,1,1},8{1,0,0},9{0,0,1},10{0,0,1},11{1,1,0},12{0,1,1},13{1,1,1},14{0,1,1},15{0,1,0}},VertexShifts{1{0,1,0},2{1,1,1},3{0,1,0},4{0,0,1},5{0,0,0},6{0,1,0},7{1,1,0},8{0,1,0},9{0,0,0},10{0,0,0}},Epsilon{10,20,30,40,50,61,71,80,91,100,110,121,130,141,150},EdgePairs{1{{0,0,1},{0,1,0}},2{{0,0,1},{1,1,1}},3{{0,1,0},{1,1,1}},4{{0,0,0},{1,1,1}},5{{0,0,0},{1,1,0}},6{{1,1,0},{1,1,1}},7{{0,0,1},{1,1,0}},8{{0,1,0},{1,1,0}},9{{0,0,0},{0,0,1}},10{{0,0,0},{0,0,1}},11{{0,0,1},{1,1,1}},12{{0,0,1},{0,1,0}},13{{0,0,1},{1,1,0}},14{{0,0,1},{0,1,0}},15{{0,0,0},{0,1,0}}},IndexedCycles{{{0,0,0},{24,25,49,510,910}},{{0,0,1},{13,14,35,49,510,67,610,78,89}},{{0,1,0},{13,16,38,610,89,910}},{{1,1,0},{25,27,35,38,78}},{{1,1,1},{14,16,24,27,67}}},CycleDoubleCover{{24,25,49,510,910},{13,14,35,49,510,67,610,78,89},{13,16,38,610,89,910},{25,27,35,38,78},{14,16,24,27,67}},Checks{Equation4True,EndpointAgreementTrue,LocalParityTrue,EveryEdgeTwiceTrue}}
In[]:=
cycleDoubleCoverPicture[GraphData[snarks[[1]]],"CycleDoubleCover"/.pete]
Out[]=
That worked. We may as well do ALL OF THE SNARKS.
In[]:=
cleansnarks=Table[Graph[Range[GraphData[snarks[[k]],"VertexCount"]],GraphData[snarks[[k]],"EdgeList"],VertexCoordinates->Thread[Range[GraphData[snarks[[k]],"VertexCount"]]->GraphData[snarks[[k]],"VertexCoordinates"]]],{k,1,372}];
In[]:=
more=Monitor[Table[cycleDoubleCoverData[cleansnarks[[k]]],{k,1,372}],k];
In[]:=
Manipulate[cycleDoubleCoverPicture[cleansnarks[[k]],"CycleDoubleCover"/.more[[k]]],{k,1,372,1},SaveDefinitions->True]
Out[]=
​
k
And it seems to work with all of them. That’s not a verification of the proof, but it’s decent evidence.

CITE THIS NOTEBOOK

Get snarky: the cycle double cover conjecture -- an AI proof?​
by Ed Pegg​
Wolfram Community, STAFF PICKS, July 10, 2026
​https://community.wolfram.com/groups/-/m/t/3756327