Recently, a trio of mathematicians – Marijn Heule from the University of Texas, Victor Marek from the University of Kentucky, and Oliver Kullmann from Swansea University – have solved a problem in mathematics and the solution takes up 200 terabytes of basic text (just consider the fact that 1 terabyte can hold 337,920 copies of *War and Peace*)! This breaks the previous recorded of a 13-gigabyte proof, which was published in 2014.

The mathematics problem is named the ‘Boolean Pythagorean Triples problem’, and was posed by Ronald Graham in the 1980s, who offered a $100 prize for the solution.

The problem is part of Ramsey theory and asks:

“Is it possible to colour all the integers either red or blue so that no Pythagorean triple of integers

a,b,c, satisfying are all the same colour. For example if you would colouraandbred, andcblue, this would successfully not satisfy the tested triple, but all triples would have to be tested.”

Andrew Moseman from *Popular Mechanics* details how:

“What makes it so hard is that one integer can be part of multiple Pythagorean triples. Take 5. So 3, 4, and 5 are a Pythagorean triple. But so are 5, 12, and 13. If 5 is blue in the first example, then it has to be blue in the second, meaning either 12 or 13 has to be red.“

The proof found that it is only possible to colour the numbers in such a way up to the number 7,824 and that 10^{2,300 }such colourings exist. Hence, there is no solution to the problem question. The proof took a supercomputer two days to solve, and generated 200TB of data!

The paper describing the proof was published on arXiv on the 3rd of May 2016.

Although the computer has proved that the colouring is impossible, it has not provided the underlying reason why this is, or explored why the number 7,824 is important. This highlights the objection to the value of computer-assisted proofs; yes, they may be correct, but to what extent are they mathematics?

Let me know what you think of computer assisted proofs below! M x