Solved by Computer: Famous Maths Problems Machines Helped Crack (1976–2026)

In 1976 two mathematicians in Illinois announced they had proved that four colours are enough to colour any map — and that part of their proof could only be checked by a computer. Many mathematicians were deeply uneasy: is it really a proof if no human can read it all? Fifty years later the question has flipped. In 2026, AI systems found the key ideas behind results that experts had failed to find for decades. This article tells that story in order, and for each famous problem says exactly what the machine did — because “solved by computer” can mean very different things.

1976: Four colours, and a proof nobody could read

GCSE core The question is simple enough for a primary school: colour a map so that neighbouring countries never share a colour. How many colours might you need? Francis Guthrie guessed four in 1852. It is easy to see you can need four — look at the picture below — but proving that four is always enough, for every possible map, defeated mathematicians for 124 years.

Kenneth Appel and Wolfgang Haken found a way to show that any map needing five colours would have to contain one of almost two thousand special patterns, and that each of those patterns can be “reduced” away. Checking all of them by hand was impossible, so a computer did it, using over a thousand hours of machine time. The theorem was proved — but in a way that changed what “proof” meant in practice.

How the doubt was settled: a shorter computer proof followed in 1996, and in 2005 Georges Gonthier and Benjamin Werner checked the entire argument inside the Coq proof assistant. Today it is one of the most thoroughly verified theorems in mathematics.

1996: the first proof a computer found on its own

Undergraduate extension The Robbins conjecture asked whether three short rules describe exactly the same algebra as Boolean algebra — the true/false logic inside every computer chip. Top logicians, including Alfred Tarski, had failed to settle it for sixty years. In 1996 William McCune's automated theorem prover, EQP, searched through possible chains of reasoning for about eight days and found a proof. This was different in kind from 1976: nobody had told the computer what the argument should look like.

1998–2014: Kepler's oranges

In 1611 Johannes Kepler claimed that the way greengrocers stack oranges — each layer sitting in the hollows of the one below — is the densest possible packing of equal spheres. It fills about 74% of space (exactly π/√18).

Thomas Hales, with Samuel Ferguson, converted the question into thousands of optimisation problems and solved them by computer, announcing a proof in 1998. The journal's referees said they were “99% certain” it was correct but could not check every calculation. Hales responded by leading the Flyspeck project to re-check everything in proof-assistant software; it finished in 2014.

2016: the 200-terabyte proof

GCSE core Here is a puzzle you can try yourself. Colour each whole number red or blue. Can you do it so that no Pythagorean triple — three numbers with a² + b² = c², like 3, 4, 5 — is all one colour?

Ronald Graham offered $100 for the answer. In 2016 Marijn Heule, Oliver Kullmann and Victor Marek used a SAT solver — software that solves enormous true-or-false logic puzzles — on the Stampede supercomputer for about two days. The answer: every number from 1 to 7,824 can be coloured safely, but 1 to 7,825 cannot. The proof that no colouring of 7,825 numbers works was 200 terabytes long — reported by Nature as the largest maths proof ever at the time. The same technique settled Keller's conjecture about tiling space with cubes in seven dimensions in 2019.

2025–2026: AI starts finding the ideas

Postgraduate extension Everything above used computers for checking or for searching within a framework humans designed. From 2025, systems built on large language models began proposing the mathematical ideas themselves — and pairing them with the proof assistant Lean, so that the output could be machine-checked rather than simply trusted.

The unit distance conjecture (May 2026). In 1946 Paul Erdős asked: if you place n points on a flat surface, how many pairs can be exactly 1 unit apart? He believed the answer grows only a tiny bit faster than n. An internal OpenAI model found an infinite family of point sets that beats that by a genuine power of n, using deep tools from algebraic number theory. Nine leading mathematicians — including Fields Medallists Tim Gowers and Jacob Tsimerman — checked it and wrote a companion paper, and Will Sawin made the gain explicit. Gil Kalai compared its importance to the Four Colour proof of 1976.

AlphaProof Nexus (May 2026). Google DeepMind ran its agent, which combines the Gemini model with Lean, on 353 open problems from the Erdős problems database. It solved 9 — including two open for 56 years — and proved 44 conjectures from the Online Encyclopedia of Integer Sequences. Every proof compiles in Lean. Notice the success rate, though: roughly 2.5%.

Astra (August 2026). OpenAI announced ten results from its unreleased next model, including the first construction of a non-sofic group (answering a question Mikhail Gromov raised in 1999), three Erdős problems and the first improvement since 1978 to a general sphere-packing bound. Each came with a Lean certificate. An independent human audit found no confirmed substantive errors in the main results, though one result drew a specialist request for major revision, and journal peer review had not concluded at the time of writing.

Fifty years in one timeline

What this means if you are learning maths

Every result in this article still depended on people: someone had to state the problem precisely, decide which approach was worth running, check that the theorem the computer proved was the theorem that mattered, and explain why it is true. That is exactly the skill school maths builds when it asks you to show your working — and it is the theme of our article Can AI Actually Do Maths?. For the problems that are still open, and a card-by-card list of these solved ones, see our Unresolved Mathematical Mysteries hub.