http://www.newscientist.com/article/dn25068-wikipediasize-maths-proof-too-big-for-humans-to-check.html
Wikipedia-size maths proof too big for humans to check
17:38 17 February 2014 by Jacob Aron
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.
Wikipedia-size proof
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.
It would take years to check the computer's working – and extending the
method to check for yet higher discrepancies might easily produce proofs
that are simply too long to be checked by humans. But that raises an
interesting philosophical question, says Lisitsa: can a proof really be
accepted if no human reads it?
Non-human mathematics
Gil Kalai of the Hebrew University of Jerusalem, Israel, says human
checking isn't necessary for a proof to stand. "I'm not concerned by the
fact that no human mathematician can check this, because we can check it
with other computer approaches," he says. If a computer program using a
different method comes up with the same result, then the proof is likely
to be right.
Kalai was part of a group that decided in 2010 to work on the problem as
a Polymath project, an exercise in which mathematicians use blogs and
wikis to collaborate on a large scale. Running different software, the
group managed to test a sequence of length 1124 – close to the threshold
Konev and Lisitsa have now shown was necessary – but gave up when the
program wouldn't scale to higher numbers.
When it comes to the Erdős discrepancy problem, there is still some hope
for humans, however. Erdős's hypothesis was that a discrepancy of any
value can always be found, a far cry from the discrepancies of 1 and 2
that have now been proven. Lisitsa's software has been running for weeks
in an attempt to find a result for discrepancy 3. But even if subsequent
programs show that higher and higher discrepancies exist for any
infinite sequence, a computer cannot check the infinity of all numbers.
Instead, it's likely that computer-assisted proofs for specific
discrepancies will eventually enable a human to spot a pattern and come
up with a proof for all numbers, says Lisitsa. "The outstanding problems
are like lighthouses; they give us targets for our abilities," adds Kalai.
Reference: arxiv.org/abs/1402.2184
--
((Udhay Shankar N)) ((udhay @ pobox.com)) ((www.digeratus.com))
