Mathematics is a subject that dates back thousands of years. Central to the subject is the idea of proof, a rigorous, step-by-step argument, starting from a few basic facts accepted as true, that conclusively demonstrates that a statement is true. Over the past few decades, however, the use of computers to prove statements has transformed the way mathematicians think about proof – and created controversy in the field.

Imagine taking the positive whole numbers, 1, 2, 3, … up to and including some number N, and colouring each number either red or blue. We impose a constraint: no three numbers of the same colour can form a Pythagorean triple; that is, if a, b, c satisfy the equation a^2 + b^2 = c^2 then a, b and c cannot all be the same colour. The question is: can we do this for any number N?

This mathematical problem is called the Boolean Pythagorean triples problem, and for decades the answer was unknown, until three mathematicians found a solution in 2016. It turns out that a colouring is not always possible – the smallest N for which no valid colouring exists is 7825.

“If a proof of the Riemann hypothesis were written in Linear A, would we consider it a proof? Would we believe it?”

The proof of this was an example of a computer-assisted proof. The mathematicians were able to reduce the number of possible colourings that had to be checked to around one trillion (1 000 000 000 000), then they used a supercomputer to test each possibility. The full proof is 200 terabytes in size, making it the largest ever created at the time.

Just how large is 200 terabytes? It’s approximately the storage capacity of 400 iPhone Pro Maxes (total cost: £560 000). It’s enough to hold the full text of all 6.2 million English Wikipedia articles – 10 000 times over.

200 terabytes is, in short, too much for any human to read, let alone comprehend, and this problem is far from the only mathematical result with a proof that relies on computers. Another example is the Kepler conjecture, about the most efficient way to pack spheres. Thomas Hales announced a proof in 1998, but since no one could verify the code used, it was not until 2005 that the proof was formally accepted.

The earliest, and most famous, example dates back to 1976, when Appel and Haken announced a proof of the four colour theorem. This theorem states that (subject to certain conditions) any map can be coloured with at most four colours such that no two bordering regions have the same colour. For example, it is possible to colour the lower 48 states of the US in this way. Their 1000-page proof involved checking 1478 configurations with a computer. Appel and Haken’s proof was very controversial at the time, and while simplifications have since been found, there is still no proof (and may never be) that is fully understandable by humans.

“If a proof involves a computer program that no human has checked, how sure can we be that it is correct?”

It is clear that computers have changed mathematics. But have they changed it for better, or for worse? Are proofs no human can check really proofs at all? These philosophical questions go to the heart of the purpose of proofs, and the proof of mathematics in general.

Many mathematicians argue that the purpose of a proof is not just to yield the result, but to understand it – something that computer-based proofs lack. “Mathematicians think they are building theories with the ultimate goal of understanding the mathematical universe,” says Minhyong Kim, a professor at Oxford. An analogy might be a proof written in an undeciphered language – if a proof of the Riemann hypothesis (an important unsolved problem) were written in Linear A, would we consider it a proof? Would we believe it?

This leads to a second concern: if a proof involves a computer program that no human has checked, how sure can we be that it is correct? A proof that involves tens of thousands of lines of code could easily contain bugs, any one of which might invalidate the entire result.

Other mathematicians, however, have embraced the use of computers. They point out that arguments given against computer-assisted proofs often apply to human ones too. Mistakes can and have occurred, and modern proofs often rely on previous results which rely on previous results, to the point where mathematicians may use results whose proofs they have not themselves checked. In a talk, Kevin Buzzard, a professor at Imperial College London, argued that no single person understands the entire proof of Fermat’s Last Theorem, and even went as far as to claim that it is possible (though unlikely) that large numbers of accepted mathematical results are in fact false.

Buzzard, alongside other mathematicians like Vladimir Voevodsky, proposes a solution: the use of proof assistants (also called interactive forum provers) to verify mathematical results. These are computer programs (of which there are many, such as Lean or Coq) designed to check every step of a proof by entering them in a program; they will only be accepted if they are logically consistent. This involves starting with a small number of statements that are accepted as true (an example in geometry would be that there is a straight line between any two points), and from there, building mathematics from the ground up.

Formalising all of mathematics like this would be a colossal endeavour, and we are nowhere near this happening. But the consequences of this would be profound. What could come after? Buzzard writes: “One day we will surely experience ‘Appel and Haken II’ – where a computer announces a proof of a conjecture which humans are interested in, and if the argument is sufficiently deep then the computer might not be able to explain their argument using a language that humans can understand.” That might be decades away, but if it does happen, it would be the most significant development in mathematics – a science thousands of years old – ever.