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.

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

I don’t know what an SAT-solver-based proof is but I am not terribly impressed when Professor kalai can only manage “the proof is likely to be right”. This is mathematics not quantum physics.

An SAT solver solves the Boolean satisfiability problem – for a given formula in Boolean logic, find values for the variables such that the formula evaluates to

true.I wrote the “fruit” explanation of the project and have been working on the problem for a while.

First off, note that the computer proof was essentially (and in at least one bit, literally) like solving a giant Sudoku puzzle. We’d been trying very hard to generate a sequence longer than 1124 — as mentioned in my original post, we tried hard enough to assume that it *was* the hard limit — so getting up to 1160 was an accomplishment in itself, and the sequence is checkable by hand.

The thing that required a computer is checking there was no longer sequence. However,

I think you’re correct the computer generated explanation why 1161 to break a discrepancy of 2 is required is not terribly satisfying, but we have a better picture of the mathematical universe this problem lives in and assuming we take another crack at it, we should have easier time asking “why 1161” (given that before we were asking “why 1125” which was flat-out wrong).