Filed under:

A computer made a math proof the size of Wikipedia, and humans can't check it

If you buy something from a Verge link, Vox Media may earn a commission. See our ethics statement.

If you thought the mathematical proofs you did in high school were long, you haven't seen the newest one out of the University of Liverpool — computer scientists Alexei Lisitsa and Boris Konev came up with a math proof that takes up a huge 13-gigabyte file, greater than all of Wikipedia's pages combined, that humans physically can't check.

It's a big step forward in solving Erdős discrepancy problem, which was proposed by Hungarian mathematician Paul Erdős in the 1930s. Erdős imagined an infinite sequence of numbers containing nothing but +1s and -1s, and he wanted to see the sequence's capacity to contain internal patterns. He came up with a way of measuring this by cutting the infinite sequence at a point and creating smaller subsequences within it (such as considering only every third or fourth number). Adding up the numbers of a subsequence provides a figure called the discrepancy, which acts as a measure of the subsequence's structure as well as the entire infinite sequence.

This proof belittles the Enormous Theorem's 15,000 pages

Erdős' main hypothesis was that a discrepancy of any value can always be found, but he was never able to prove it. New Scientist explains that it's fairly easy to prove a discrepancy of 1 using just 12 pluses and minuses, but extending the method to higher discrepancies gets complicated as the number of subsequences increase. But Lisitsa and Konev were able to use a computer in this experiment to "prove" an infinite sequence will always have a discrepancy of 2 or more. However, doing so took the computer six hours and produced a proof longer than the 15,000-page Enormous Theorem.

Trying to check this proof would be an inhuman task — and if checking a proof with a discrepancy of 2 is this difficult, it would be impossible for a human to check any proofs with higher discrepancies. It raises the question of non-human mathematics: if a proof can only be checked with a computer, can it be accepted as true by humans? According to Gil Kalai of the Institute of Mathematics at the Hebrew University of Jerusalem in Israel, a human might not have to check it. He claims that if another computer can generate the same proof with the same results, it's likely to be accurate.

Lisitsa and Konev have already moved on to the next project — their computer has been running for weeks to try to find a result for a discrepancy of 3.