If no human can check a proof of a theorem, does it really count as mathematics? That's the intriguing question raised by the latest computer-assisted proof. It is as large as the entire content of Wikipedia, making it unlikely that will ever be checked by a human being.
"It might be that somehow we have hit statements which are essentially non-human mathematics," says Alexei Lisitsa of the University of Liverpool, UK, who came up with the proof together with colleague Boris Konev.
The proof is a significant step towards solving a long-standing puzzle known as the Erdős discrepancy problem. It was proposed in the 1930s by the Hungarian mathematician Paul Erdős, who offered $500 for its solution.
Imagine a random, infinite sequence of numbers containing nothing but +1s and -1s. Erdos was fascinated by the extent to which such sequences contain internal patterns. One way to measure that is to cut the infinite sequence off at a certain point, and then create finite sub-sequences within that part of the sequence, such as considering only every third number or every fourth. Adding up the numbers in a sub-sequence gives a figure called the discrepancy, which acts as a measure of the structure of the sub-sequence and in turn the infinite sequence, as compared with a uniform ideal.
Erdős thought that for any infinite sequence, it would always be possible to find a finite sub-sequence summing to a number larger than any you choose - but couldn't prove it. It is relatively easy to show by hand that any way you arrange 12 pluses and minuses always has a sub-sequence whose sum exceeds 1. That means that anything longer – including any infinite sequence – must also have a discrepancy of 1 or more. But extending this method to showing that higher discrepancies must always exist is tough as the number of possible sub-sequences to test quickly balloons.
Now Konev and Lisitsa have used a computer to move things on. They have shown that an infinite sequence will always have a discrepancy larger than 2. In this case the cut-off was a sequence of length 1161, rather than 12. Establishing this took a computer nearly 6 hours and generated a 13-gigabyte file detailing its working. The pair compare this to the size of Wikipedia, the text of which is a 10-gigabyte download. It is probably the longest proof ever: it dwarfs another famously huge proof, which involves 15,000 pages of calculations.