Boris Konev and Alexei Lisitsa of the University of Liverpool have been looking at sequences of $+1$s and $-1$s, and have shown using an SAT-solver-based proof that every sequence of $1161$ or more elements has a subsequence which sums to at least $2$. This extends the existing long-known result that every such sequence of $12$ or more elements has a subsequence which sums to at least $1$, and constitutes a proof of Erdős’s discrepancy problem for $C \leq 2$.

Erdős’s discrepancy problem deals with infinite sequences of $+1$s and $-1$s. It asks whether or not a finite subsequence exists which sums to a given integer $C$; since you’d expect every $+1$ to be cancelled out by a $-1$ at some point, the non-zero sum $C$ is called a ‘discrepancy’. To narrow things down, the problem only looks at subsequences which use entries taken at regular intervals from the start.

More formally, the problem asks for a proof or disproof of the following statement:

For any infinite $\pm 1$-sequence $( x_1, x_2, \ldots )$ and any integer $C$, there exist integers $k$ and $d$ such that

\[ \left\lvert \sum_{i=1}^k x_{i \cdot d} \right\rvert \gt C \]

For a simpler outline of the statement, try Jason Dyer’s blog post, which explains it in terms of fruit (and was written back in 2010, when the suspected length needed for discrepancy $2$ was $1125$).

For an even more understandable statement of the problem and recent work, which includes a fab rephrasing of it as a puzzle, you can always rely on a YouTube video from James Grime.

[youtube url=http://www.youtube.com/watch?v=pFHsrCNtJu4]

The story was covered in The Independent, with the usual photo of cumulonumbers, and the classic ‘boffins crack puzzle’ attitude – in fact, they fail to explain that the sequences involved don’t have to be consecutive entries, making it difficult to understand what has actually been proved (there was some discussion on Twitter). Amusingly, the amount of data processed in proving the result was a whopping 13Gb – as described by the article, ‘larger than the size of all the text on Wikipedia’, or as a normal person would say, ‘small enough to fit on any modern home computer’s hard drive a few times over’.

For better coverage, with actual explaining, check out the New Scientist article, which focuses on the fact that this proof is so large it’s impossible for a human to verify it – a fact that’ll annoy some people. This is nicely tied up with the following quote attributed to Gil Kalai:

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.

Further Reading:

A SAT Attack on the Erdos Discrepancy Conjecture by Boris Konev and Alexei Lisitsa

Boris Konev’s academic homepage

Alexei Lisitsa’s academic homepage

The Erdős discrepancy problem explained at the Polymath wiki

Computer cracks Erdős puzzle – but no human brain can check the answer at The Independent

Wikipedia-size maths proof too big for humans to check at New Scientist

Computers are providing solutions to math problems that we can’t check at io9 (a cut-down version of the New Scientist piece)

Recent news concerning the Erdos discrepancy problem on Tim Gowers’s blog

New Wikipedia sized proof explained as a puzzle by James Grime on YouTube