The Biggest Mathematical Proof Ever
Sophie Maclean
In the current age of advancing AI, most mathematicians have been asked at some point (often by a well-meaning student or journalist), “Could this problem be solved by a computer?” More often than not, the answer is no. But occasionally, the answer is yes.
One famous example of a theorem that was proved with the help of a computer is the four-colour theorem. This theorem asks whether any map can be coloured in at most 4 colours, such that no two regions sharing an edge (or part of an edge) are the same colour. The answer is yes, and the way that mathematicians proved it was by simplifying the problem into a finite number of cases to check, and getting a computer to check them.
Many people are unsatisfied with this as a mathematical proof. They claim it gives no deep insight into why the theorem is true. In the other camp, some believe that regardless of whether you like the proof or not, it is a valid proof and gives us the answer to the question. Goal achieved.
In the case of the four colour theorem, there were about 2000 cases to check, which took a computer in the 1970s about 1000 hours to go through. At the time, this would have been a big calculation. But as computers have gotten more and more powerful, they can be used to do bigger and bigger calculations.
In 2017, the record for the largest mathematical proof hit a new high. Using a computer, a theorem was proven in a proof that used 2 petabytes of space. That is \(2 \times 10^{15}\) bytes of space. It is this problem that I would like to share with you today.
A Puzzle
Take the numbers 1 to 5. Can you colour them into two colours with the property that no two (not necessarily distinct) numbers of one colour sum to a third of the same colour? Have a go and see what you notice!
Whilst you are thinking, it may also interest you to learn that mathematicians generally describe this property (having two numbers adding to a third of the same colour) as there being a monochromatic \(x + y = z\).
The first thing you may realise is that 1 and 2 have to be in different colours because 1 + 1 = 2. Let us call our sets Apricot and Blue (or A and B, for short). We currently have:
A: 1
B: 2
It is natural now to think about where 3 might go, but I want to jump ahead and consider number 4. 2 + 2 = 4, so we therefore must colour 4 in Apricot:
A: 1, 4
B: 2
Now let us consider 3. 1 + 3 = 4, so we need to colour 3 in Blue.
A: 1, 4
B: 2, 3
But now we have a problem. 1 + 4 = 2 + 3 = 5. 5 cannot be either colour.
So it’s impossible to colour the numbers 1 to 5 in two colours as described. This means that it is impossible to colour the numbers 1 to N into two colours without a monochromatic \(x + y = z\) for any N >= 5 (as that would necessitate doing the above).
What about if we look at colouring the numbers 1 to N in 3 colours (again with no two numbers of one colour summing to a third)? Can we do it when N is 5? 10? 20? I will spoil this one for you – we can do it for N up to 13, but not for \(N \geq 14\).
If you want a challenge, see if you can find a way of colouring the numbers 1 to 13 in three colours with no monochromatic \(x + y = z\). It is possible, but not easy!
To Infinity…
A question we often ask as mathematicians is “how can we generalise this?” In this case, the natural question is whether, for any number of colours, we have that as long as N is large enough, it is impossible to avoid a monochromatic \(x + y = z\).
Writing this more mathematically, our question is
“For every \(k>0\), does there exist \(N>0\) such that if the set \(\{1, 2, \dots, N\}\) is partitioned into \(k\) sets (labelled \(s_1, s_2, \dots, s_k\) ), there exists \(x, y, z \in s_i\) (not necessarily distinct) with \(x + y = z\).”
The exciting news is, we have an answer to this question! Over 100 years ago, in 1917, Issai Schur proved that the answer is yes. We will go over his proof, but first, we need to take a brief foray into Ramsey Theory.
Ramsey Theory is a branch of graph theory and combinatorics – the maths of counting. As a quick introduction (or refresher) into graph theory, a graph is a series of vertices connected by edges. Ramsey Theory is, in particular, concerned with how many vertices a graph needs to have for certain properties to be present.
The result we need is a version of Ramsey’s Theorem. This theorem concerns graphs with all possible edges drawn in, known as the complete graph. The complete graph with n vertices is denoted \(K_n\).
Ramsey’s Theorem tells us a few things, but the relevant outcome here is that if we colour the edges of a complete graph, \(K_n\), one of r colours, then, so long as n is big enough, it is impossible to avoid a monochromatic triangle (i.e. a triangle in which all edges are the same colour).
Let’s write \(T(r)\) to mean the smallest n such that a monochromatic triangle is guaranteed in an r-coloured \(K_n\). Another way of interpreting the above fact is that Ramsey’s theorem guarantees that \(T(r)\) exists for all \(r\).
… and Beyond
With this information, we can prove Schur’s Theorem! Remember, what we’re looking for is a proof that for any \(k\), there exists an n such that if we colour \(\{1,2,\dots,n\}\) in \(k\) colours, there is always a monochromatic \(x + y = z\).
What I’m actually going to do is go on better than this. I will show that actually, if \(n = T(k)\), then if we colour \(\{1,2,\dots,n\}\) in \(k\) colours, there is always a monochromatic \(x + y = z\). So let’s suppose we have a colouring. Every natural number up to \(T(k)\) is coloured one of \(k\) different colours, let’s call them \(c_1, c_2,\dots, c_k\).
We are now going to construct a graph. Each vertex of this graph will be labelled with a different number from \(1\) to \(T(k)\). Now let’s draw in all the edges, to give us the complete graph \(K_{T(k)}\), and we will colour the edges according to the difference of their vertices. What I mean by this is that if the vertices are labelled a and b, then we will colour the edge between \(a\) and \(b\) whatever colour \(|a-b|\) is in our colouring of \(\{1,2,\dots, T(k)\}\).
This is where the magic comes in. Ramsey’s Theorem tells us that because the graph is \(T_{k}\), and the edges are one of \(k\) colours, then there must be a monochromatic triangle. Let’s suppose that the vertices of this triangle are \(i, j,\) and \(k\), with \(i > j > k\). By the way we have coloured the edges, \(x = i – j\), \(y = j – k\), and \(z = i – k\) are all the same colour in our colouring of \(\{1,2,\dots, T(k)\}\). We also know that \(x + y = z\). So there must be a monochromatic \(x + y = z\).
Yay! We are done. We have proven that for any k, there exists an n such that if we colour \(\{1,2,\dots,n\}\) in \(k\) colours, there is always a monochromatic \(x + y = z\). This is known as Schur’s Theorem.
Schur Numbers
Those paying extra close attention will have noticed that there is still one thing we don’t know. Although we know that there exists an n with our magic property, we do not know what that n could be. Really, the number of interest is the smallest n such that if we colour \(\{1,2,…,n\}\) in k colours, there is always a monochromatic \(x + y = z\). Let’s call this \(n\), \(S(k)\). As you may have guessed, the S stands for Schur, and these numbers are called Schur Numbers.
Our above reasoning tells us that \(S(k)\) is at most \(T(k)\), but it does not preclude the possibility that it is smaller. You will be unsurprised to learn that \(S(1) = 2\). Because 1 + 1 =2. Straight off the bat, we have proved that it is not necessarily true that \(S(k) = T(k)\). S(1) is already smaller than \(T(1)\), which equals 3, as all triangles have at least 3 sides.
We also already know that \(S(2) = 5\), too, as this is what we showed earlier. And I told you that \(S(3) = 14\). Beyond that, it gets tricky. It took until 1965 for it to be shown that \(S(4) = 44\). But then people got stuck. At the turn of the millennium, \(S(5)\) still hadn’t been found.
To find an \(S(5)\), we needed a new strategy. If you cast your mind back to the introduction, you might be able to guess what this new method is. Use a computer. Or rather, use a computer cleverly.
After a lot of work, it was strongly suspected that \(S(5)= 161\) but to prove this requires two things: showing that there is an n for which any 5-coloured \(\{1, 2, \dots, 161\}\) must have a monochromatic \(x + y = z\), and also showing that \(161\) is the smallest such n with this property. The second part is equivalent to finding a colouring of \(\{1, 2, \dots, 161\}\) without a monochromatic \(x + y = z\).
The second part is easier: Once you have found an example, you can move on. We now know that there are exactly 2,447,113,088 such 5-colourings, so it is not too difficult to find one. Proving that any 5-colours \(\{1, 2, \dots, 161\}\) has a monochromatic \(x + y = z\) is much trickier.
Obviously, with a computer, in theory, one could just check every case. But let’s follow this line of reasoning through. There are \(5^{161}\) possible colourings. This is about \(3.4 \times 10^{112}\), which is greater than the number of particles in the universe, so we are already not off to a great start. There are about \(3.1 \times 10^7\) seconds in a year. So even if we could check a million cases in a second, it would take us \(10^{99}\) years to get an answer. That is 10 with 99 zeros after it. To put this in perspective, the universe is only \(10^9\) years old.
Luckily for us, the computer scientists and logicians have come to the rescue. Specifically, Marijn Heule, Dutch computer scientist at Carnegie Mellon University, turned his hand to solving the problem.
Heule is an expert in a rather fiddly technique, which can determine whether or not a certain type of problem has a solution. This kind of computer program is called a SAT solver (where SAT is short for satisfiability). It would take a whole lecture course to satisfactorily (pun intended) explain what a SAT solver is and how it is used here, but in short the question of what is S(5) was turned into a series of boolean logic formulas, which take a series of TRUE and FALSEs as inputs, and output a TRUE or FALSE.
Armed with his expertise in SAT solvers, Heule set to work. After much toiling, he had done it. New technology had to have been invented, but S(5) had finally fallen. The proof was not any old proof though. Combined, the proof used 2 petabytes of space. This is the record-breaking proof that I promised.
So, in 2017, exactly 100 years after Schur’s original proof, it was finally known. \(S(5) = 161\).
The post The Biggest Mathematical Proof Ever originally appeared on the HLFF SciLogs blog.