Computers have been generating proofs for mathematical statements for years. However, none has ever come close to the length of the proof of the Boolean Pythagorean triples problem.
A Pythagorean triple is a set of three whole numbers that satisfy a2 + b2 = c2. This is the equation most commonly used to find the lengths of the sides of a right angled triangle. For example, the triple 32 + 42 = 52 could describe a triangle with two sides of lengths 3 and 4 at right angles to each other, and the longest edge with length 5.
The Boolean Pythagorean triples problem was set by Ronald Graham in the 1980s, and asks whether it is possible to assign all positive whole numbers a colour of either blue or red, so that no three numbers in any Pythagorean triple have the same colour.
The problem is harder that it looks. Some integers are part of many Pythagorean triples, for example 5 is in the triple 3, 4, 5 as well as 5, 12, 13. If 5 is allocated the colour blue in the first triple, it must stay blue in the second, and either 12 or 13 or both must then be red. This carries on into the much higher numbers, and the team have shown that this task eventually becomes impossible at the number 7,825.
Scientists Marijn J. H. Heule, Oliver Kullmann and Victor W. Marek solved the problem – finding this limit – using the Cube-and-Conquer program. This searches all the possible solutions by placing them into cubes. Working through all of the combinations up to that limit would be impossible by hand; the original proof takes a whopping 200TB of storage space, about the capacity of 46,600 DVDs.
Even now, the solution is much too long to ever be read and verified by a human; the shortened version produced by the team would take 30,000 hours for a computer to process.
There are 102,300 possible ways to colour the integers up to 7,825, and even after a load of mathematical tricks were applied, from symmetry to number theory techniques, there still were a trillion combinations to check.
To find the solution, the team used the University of Texas’ Stampede Supercomputer, which ran 800 processors for two days.
Even though the problem has now been solved, and verified by another computer program, it doesn’t add much to our understanding of the problem, begging the question ‘is this a real proof?’. Previous use of computers to prove mathematical problems has later been verified by hand, but in this case it simply cannot be done. A real proof should improve our understanding of the problem, but we still don’t understand why colouring the integers works until 7,824 but stops there.
It’s a cool achievement, but in reality we have gained no further understanding of the problem and can’t solve similar problems any more easily.
The solution is little more than a useless fact.
If you have any comments or questions about this subject, please direct them to firstname.lastname@example.org
Photo Credit: A Makris