*arXiv*, the two describe how they set a computer program to proving a small part of what's known as "Erdős discrepancy problem"—the proof produced a data file that was 13-gigabytes in size—far too large for any human to check, leading to questions as to whether the proof can be taken as a real proof.

Anyone who has taken a high level math course can attest to the fact that math proofs can sometimes grow long—very long. Some mathematicians have dedicated years to creating them, filling whole text volumes in the process. Quite naturally then, mathematicians have increasingly turned to computers to perform some of the more mundane parts of proof creation. It wasn't long, however, before some began to realize that at some point, the proofs spit out by the computer would be too long, complicated or both for a human reader to fully comprehend. It appears, with this new effort that that day might have come.

Erdős discrepancy problem revolves around trying to find patterns in an infinite list of just the two numbers "1" and "-1". Named after Paul Erdős, the discrepancy problem arises when cutting off the infinite sequence at some point and then creating a finite sequence using a defined constant. When the numbers are added up, the result is called the discrepancy figure. Lisitsa and Konev entered the problem (with a discrepancy constant of 2) into a computer running what they describe as state of the art SAT solvers—software that has been written to create mathematical proofs. The proof that the computer came up with proves, the two researchers claim, "that no sequence of length 1161 and discrepancy 2 exists."

Unfortunately the file produced was too large to read—for comparison's sake, it was a couple of gigabytes larger than the whole of Wikipedia. This leads to an interesting conundrum for mathematicians going forward. Do we begin accepting proofs that computers create as actual proofs if they are too long or perhaps too difficult for our minds to comprehend? If so, we might just be at a crossroads. Do we trust computers to handle things for us that our beyond our abilities, or constrain our reach by refusing to allow for the creation of things that we cannot ever possibly understand?

**Explore further:**
Mathematician announces that he's proved the ABC conjecture

**More information:**
A SAT Attack on the Erdos Discrepancy Conjecture, arXiv:1402.2184 [cs.DM] arxiv.org/abs/1402.2184

**Abstract**

In 1930s Paul Erdos conjectured that for any positive integer C in any infinite +1 -1 sequence (x_n) there exists a subsequence x_d, x_{2d}, ... , x_{kd} for some positive integers k and d, such that |x_d + x_{2d} + ... + x_{kd}|> C. The conjecture has been referred to as one of the major open problems in combinatorial number theory and discrepancy theory. For the particular case of C=1 a human proof of the conjecture exists; for C=2 a bespoke computer program had generated sequences of length 1124 having discrepancy 2, but the status of the conjecture remained open even for such a small bound. We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solvers, one can obtain a sequence of length 1160 with discrepancy 2 and a proof of the Erdos discrepancy conjecture for C=2, claiming that no sequence of length 1161 and discrepancy 2 exists. We also present our partial results for the case of C=3.

## Eikka

## IamVal

I mean, the only way to build to any particular discrepency is to have that discrepency leading and then alternating positive and negative nodes that quantify to 0. You can't have a quantity of 0 with any amount of nodes that isn't even. soo, 1161-2 = 1159 isnt even so no sequence of 1161 nodes has a discrepency of 2... or am I missing something?

## IamVal

## krundoloss

This reminds me of "The Matrix", when the Agent Smith says "This is the peak of your society. I say 'your society' because once we began thinking for you, it really became 'our society'."

I think we can trust computer generated proofs because they so calculation intensive. If the computation arrives at a result that makes sense, it most likely is correct, since it was done using hardware and software designed specifically for huge calculation tasks.

## Protoplasmix

## fmfbrestel

## julianpenrod

You can avoid the need for such huge computations by simply devising a theory. A branch of the discipline being studied involving the concepts you are specifically examining, complete with theorems that describe the entire nature of the subject, even out to infinity. You don't need to look at every prime larger than 2 to know it's odd, because, if it was even, it would be divisible by 2 and so not be prime. An early instance of listing all instances was proving there are only five Platonic solids using Euler's Formula, which is universal, and seeing all the cases that satisfy. In the '70's, they proved the 4 Color Map Problem by generating a list of all possible map configurations. Computers can give great latitude of action, but they can cause many to forget the value of deriving universal laws that can answer questions, or replace long conventional proofs, in a snap.

## russell_russell

New Short Cut Found For Long Math Proofs

http://www.nytime...wanted=1

Seriously though, can you find research debunking this 1992 claim?

## ChangBroot

## alaberdy

## cabhanlistis

## ziphead

Who cares what humans think?

Other machines will accept it and (if need be) verify it.

## pepe2907

I think - no, and if it's "no" then we already rely on partial comprehension, partial proofs done by different people and breaking complex things to simpler comprehensible parts /how this is different?/.

And if a step by step process of proving parts of mathematics works we still believe in its robustness and integrity.

Am I wrong?

## pepe2907

And maybe for the specific case the answer is "no". If so then it may be checked by several solvers and ruled as "probable", "computer proven" - not so unthinkable, there are still probable theorems even in basic math without actually being properly proven.

## dtxx

Traction control and ABS on cars or how about computer automated quant-trading as a few of a billion possible examples? We are not at any such crossroads. We crossed it long ago.

## Kedas

## alfie_null

Easy. Just re-run the process. Use different equipment if you wish. If you suspect a flaw in the logic, have others examine your work. There's nothing ineffably different in computers than any other tool we use.

## Yoaker

I'd say you understand it perfectly, and that the answer is no.

## scottpetersway

## Returners

I disagree.

If something is true, then it is true whether or not anybody understands it.

## Eikka

That's why cars still have doubled unassisted hydraulic brake circuits as a failback.

Besides, these systems don't rely on mountains of data. They're very simple algorithms that can be easily understood by a single person to verify that they're doing what they're supposed to do. Even nuclear bombs were first proven on pen and paper before the numerical simulations.

The problem is, can you know that it's true?

You'd have to first prove that the proof-producing algorithm itself is absolutely flawless for all possible inputs before you could trust its output, which I believe would be such a massive undertaking that it would require the computer to prove itself... but then do you trust that proof?

And if you do, you still have to check the output for the case that the computer made a random bit error and subsequently produced 13 Gigabytes of nonsense.

## cdkeli

## cabhanlistis

Are you stating this only because the size is inconvenient for you or do you have something concrete to base this on?

## Bonia

Mar 11, 2014