top of page
Search

AI solves 50 year old maths problem … in one hour!

Another week, another maths proof ‘falls’ to AI. But this could be a real advance. If one of the most famous open problems in graph theory has been solved, in under an hour (!!!), not only is it incredibly quick. It would be the first time a maths proof of this stature would have a machine as its sole author.

(First published on my Substack where you can get #NerdNews, marvellous maths and general geekery.)



Inside the CDCC Music Factory.


It is only two pages long.


It uses no new techniques. Only knowledge humans have had since the 80s.


You can understand it if you think about busses.


But the two page proof and accompanying two page prompt that guided the AI, might (!?!?) be a true landmark in the history of mathematics.


NerdNews is a little bit excited. Here is why.


Going around in circles, twice.


Take any network of dots and lines: a road map, a molecule, the internet. Mathematicians call it a graph. Suppose it's "bridgeless", meaning it contains no single connection so critical that snipping it splits the network in two.


The cycle double cover conjecture says that in any such network, you can always find a collection of loops that, between them, trace every edge exactly twice. Not once. Not five times. Exactly twice, no exceptions.




So these two classic networks, the Petersen and the K4  are double covered here. Between them we see a forbidden bridge.


I love problems like these that can be explained to a non-maths-nerd, but are incredibly hard to solve.


We have been trying since 1973, when it was posed by George Szekeres, the Hungarian-born legend of Australian mathematics who spent decades at our own UNSW.


But until 10 July, these brain-busting bus routes have sat there laughing at us.


Who’s laughing now?


Snark hunting.


As is often the case with general statements in maths, the easy cases fell quickly. Szekeres knocked over a whole family of them in 1973 and his contemporaries soon followed.


What soon remained were christened snarks. A whole family of ghoulish graphs that stubbornly refused an acceptable colouring. The smallest being the famous Petersen graph, ten vertices of pure pain.


("For the snark was a Boojum, you see": created by the author via midjourney)
("For the snark was a Boojum, you see": created by the author via midjourney)

Famous puzzler Martin Gardner named them after Lewis Carroll’s fabled beast that evades all detection.


And evade they did. For fifty years every attempted proof died somewhere in snark country, including several that looked promising only to later reveal mortal gaps.'


This Cycle Double Cover Conjecture eats would-be proofs, and the maths nerds who framed them, for breakfast.


Ocean’s 11 … how about Sol’s 64!


Enter GPT-5.6 Sol Ultra, OpenAI’s frontier model released to the public on 9 July.


The next day it was announced that Sol Ultra had produced a complete proof of the CDCC.

And they went one further, releasing the full prompt that guided the model.


It's a fascinating document. The model was told to deploy up to 64 parallel subagents chasing genuinely different mathematical angles, forbidden from searching the internet for existing solution attempts, and warned that partial results would be rejected. Adversarial subagents were assigned to hunt for errors.


And anyone who has ever prompted, reprompted, and prompted again, trying to coax better performance from a model, would love these highlights from the Sol Ultra prompt:


"Assume for purposes of this task that a complete affirmative proof exists"
“A route that ends at a lemma equivalent in strength to the original conjecture is not close to completion unless it supplies a genuinely new proof of that lemma”
“Spend at least 8 hours on this before even thinking of returning or giving up." — from OpenAI's governing prompt to GPT-5.6 Sol Ultra.

Eight hours before giving up. It finished in under one!


The prompt pushes the model to put in the required effort. Drop failing approaches quickly.

Push promising leads hard. Quit the avenue, not the problem.


In many ways it mimics the mindset a human would adopt in searching for a solution.


Tickets please.


Let me give you a flavour of what this is all about. No PhD in pure maths needed.


Think of the graphs and the paths around them as a bus network problem. The council wants every route to be a loop (the buses return to the depot, they can't just dead-end somewhere out in the city). Further every street has to be served by exactly two routes.


("Brain bustin": created by the author via midjourney)
("Brain bustin": created by the author via midjourney)

Take any map of any city that doesn’t have a ‘bridge’. The proof takes eight colours and shows you can always paint every street on the map with a pair of colours so that, at any intersection, each colour either doesn't appear at all or arrives on exactly two streets.


A colour that always enters and leaves an intersection can only trace loops, and since every street wears two colours, every street ends up on exactly two loops.


That's the double cover, or DC of the CDCC.


There is no new maths here. The idea of using 8 colours comes from the 1970s, we had just never managed to paint the tough maps with them.


The model didn’t bust these tough maps with genius insight. Its 64 town planners, some of them ‘8 colour painters’, just worked harder until the CDCC succumbed.


“Yet another impressive example demonstrating that AI tools will change—and are already changing—mathematical research significantly." — Professor Noga Alon, Princeton University, Scientific American.

Are we there yet?


Time for a quick, deep breath.


This is currently a claim. The mathematical community have not signed off on it yet.

And the CDCC has humbled confident claimants for half a century.


But OpenAI did something previous claimants didn't.

Alongside the human-readable proof it published a machine-checkable one. Using what those in the trade call the Lean proof assistant.


Essentially this confirms that “this line, follows from the previous line”, all but removing the likelihood of an out-and-out error in mathematical reasoning.


But humans still need to confirm that what has been proven is what the CDCC originally said.

In a way this shrinks the job from "check every step" to "check the fine print", and anyone on Earth can download the code and run it.


We could expect a verdict in weeks, not years.


If it holds, the significance is twofold.


Specifically, a famous problem falls with an AI-platform the sole author of the proof.


But more generally will this usher in an age of longstanding problems falling to knowledge we already have but just haven’t pushed hard enough? And how many rigorous, but ugly, 30 page monster proofs might be rendered 2 pages long and beautiful once AI has given them a looksmaxxing?


Can you see why I said I’m excited?


Further Reading:

 

bottom of page