With news that a recent proof of the Boolean Pythagorean Triples Theorem is the ‘largest proof ever’, we collect and run-down some of the biggest, baddest, proofiest chunks of monster maths.

Russell & Whitehead’s 360-page proof that 1+1=2

“Principia Mathematica”, published in three volumes in 1910, 1912 and 1913, was a major work by mathematician and philosopher Bertrand Russell, with help from Alfred North Whitehead. The book contains a proof, starting from very basic axioms, that 1+1=2 – which takes over 360 pages! It might seem excessive, but they work from only the most basic assumptions, and have to define firstly what they mean by ‘1’, ‘2’, ‘plus’, and ‘equals’. It’s all done in formal logic, and must surely be one of the longest proofs relative to the length and complexity of the statement it’s proving.

Part of the proof, from Principia Mathematica

PROOF SIZE: 0.1148 tennis courts

Further Reading

• Principia Mathematica, on Wikipedia
• Russell and Whitehead, on The Story of Mathematics
• Restatement of the proof in more modern notation, at MetaMath Proof Explorer
• The proof starts on page 362 of Principia Mathematica Vol. 1

Proof of the Four Colour Theorem

Famously one of the first proofs that required so many fiddly cases to check that its authors resorted to a computer, the Four Colour Theorem simply states that any diagram (or equivalently, any graph) drawn on a flat piece of paper can be coloured using at most four colours, so that any two adjacent parts are different colours. The original problem was stated in 1852, and while purported proofs were published in the 1880s, they were later found to be incorrect.

The first real proof, given by Appel and Haken in 1977, roughly consisted of finding a set of 1,936 minimal reducible structures that any diagram/graph that might not be four-colourable could be made up from, then checking each one by computer. Checking the maps one by one took over 1000 computer hours, and accompanied a hand-checked component of the proof on 400 pages of microfiche.

A shorter proof, involving a mere 633 reducible structures, was produced in 1996, and that proof was formalised in 2005 using the COQ computer proof assistant, which means it’s less reliant on cases checked by computer.

PROOF SIZE: 1.8 times the area of an olympic swimming pool plus 370.4 watches of the film Avatar

Further reading

• Four Colour Theorem, on Wikipedia
• The Four Colour Theorem, at NRICH
• Formal Proof – The Four-Color Theorem, an article explaining the shorter COQ proof by Georges Gonthier in the Notices of the AMS (PDF)

Classification of Finite Simple Groups

The classification of the finite simple groups — otherwise known as ‘CFSG’ or simply The Enormous Theorem — is a bit different to the other massive proofs listed here. It’s not a single work from one person or team, but rather a joint effort among dozens of mathematicians through the (nineteen-) eighties and nineties, a patchwork of results published in separate articles which together constitute the overall theorem.

A group is roughly speaking the set of interlocking symmetries of some concrete or abstract object, and the simple ones are those that are not ‘made by’ mashing two smaller symmetry groups together. The CFSG states that any finite simple group must be either a member of one of a set of precisely-defined infinite families of groups, or one of 26 specific outliers: the sporadic simple groups.

Wikipedia reckons that the aggregated length of the papers contributing to the proof is around 10,000 pages. Work on a consolidated ‘second-generation’ proof, led by Daniel Gorenstein, is ongoing and is expected to result in an eleven-volume proof a mere 5,000 pages long. In fairness to the competition, it should be pointed out that these page counts are for the full articles/books, including all exposition as well as the bare proofs.

PROOF SIZE: 1.4 basketball courts

Further reading

• Classification of finite simple groups, on Wikipedia
• An enormous theorem: the classification of finite simple groups, by Richard Elwes at Plus Magazine
• Rewriting the enormous theorem, by Rachel Thomas at Plus Magazine
• The Status of the Classification of the Finite Simple Groups, by Michael Aschbacher (PDF)

Kepler Conjecture/FLYSPECK

The Kepler Conjecture, originally posited in the 17th century by Johannes Kepler, relates to the density of spheres packed in 3D space. Kepler conjectured that the ‘cubic close packing’ (the one where you put a hexagonal grid of spheres on a flat surface and then stack another one on top, but offset so the balls are over the gaps) is the most efficient way to pack spheres in 3D space – the one with the least empty space left in between.

While it was long suspected to be true, nobody managed to formally prove it until Thomas Hales in 1998. Hales’ proof involved around 300 pages of notes and 3 gigabytes of computer programs, data and results. It was a ‘proof by exhaustion’ which involved checking many individual cases. Referees on the proof said they were ‘99% certain’ the proof was correct, and hence that this was the most efficient 3D packing.

But that wasn’t enough for Thomas Hales – as we covered here when it was completed, the FLYSPECK project (named as it is a Formal Proof of the Kepler conjecture, and ‘flyspeck’ is a word that contains all of those letters in that order, but it’s not as good as the word ‘flapjack’) was a further project undertaken to formalise and check the previous proof. It took from its start in 2003 until September 2014 to complete, and used proof assistants Isabelle and HOL Light.

PROOF SIZE: 1.43 downloads of the film Titanic in HD, plus about 0.94 Harry Potter and the Prisoner of Azkabans

Further Reading

• The Flyspeck project is complete: we know how to stack balls!
• Git Repo for FLYSPECK
• The Kepler Conjecture, on Wikipedia

Erdős Discrepancy Problem

Another recent bit of maths that’s made headlines by having a massive proof was the Erdős Discrepancy problem – back in February 2014, a proof using an SAT solver by Boris Konev and Alexei Lisitsa of the University of Liverpool hit the headlines because it was ‘the size of Wikipedia’ (around 13 gigabytes).

The problem asks whether it’s possible to come up with an infinite sequence of +1s and -1s and a ‘target’ number in such a way that you can never get past the target by adding together regularly-spaced terms from the sequence. (Going lower than minus-the-target-number also counts, in case you thought you had trumped the proof with your clever sequence of just -1s.) James Grime has explained the problem in a video with snakes and a cliff. The proof showed that in fact you can’t always make the required sequence.

Luckily, Terence Tao came to the rescue in September 2015, with a smaller hand-crafted proof developed in collaboration with the Polymath project.

PROOF SIZE: around 3,250 holiday snaps taken on a 10 megapixel camera

Further reading

• A SAT Attack on the Erdős Discrepancy Conjecture by Boris Konev and Alexei Lisitsa
• Erdős’s discrepancy problem now less of a problem
• New Wikipedia sized proof explained with a puzzle – James Grime on YouTube
• Terence Tao has solved the Erdős discrepancy problem!

Boolean Pythagorean Triples Theorem

Claiming to be the ‘largest proof ever’, the Boolean Pythagorean Triples theorem relates to the question of whether it’s possible to split all numbers into two groups, neither of which contains a complete Pythagorean triple. For example, 3, 4 and 5 form a triple, and to find a valid split they would have to not all be in the same half – but then 5 couldn’t also be in the same half as 12 and 13, and so on.

It’s much better explained by Evelyn Lamb in her post in Nature, but a team of researchers have shown that not only is it not possible to do this, it’s not even possible to split the numbers 1 to 8000 in this way without getting stuck. It might not sound like ground-breaking mathematical knowledge we need right now, but it ties in to Ramsey Theory and other combinatorial questions. Proving it took 2 days for a computer running 800 parallel processors, and generated 200 terabytes of data.

PROOF SIZE: Amount of data generated by CERN every 2.92 days

Further reading

• Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer by Marijn J. H. Heule, Oliver Kullmann and Victor W. Marek
• Two-hundred Terabyte maths proof is largest ever, by Evelyn Lamb at Nature
• Boolean Pythagorean Triples theorem on Wikipedia