February 19, 2014 report

# Computer generated math proof is too large for humans to check

(Phys.org) —A pair of mathematicians, Alexei Lisitsa and Boris Konev of the University of Liverpool, U.K., have come up with an interesting problem—if a computer produces a proof of a math problem that is too big to study, can it be judged as true anyway? In a paper they've uploaded to the preprint server *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

**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.

© 2014 Phys.org

**Citation**: Computer generated math proof is too large for humans to check (2014, February 19) retrieved 22 September 2019 from https://phys.org/news/2014-02-math-proof-large-humans.html

## User comments

EikkaIamValI 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?

IamValkrundolossThis 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.

ProtoplasmixfmfbresteljulianpenrodYou 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_russellNew Short Cut Found For Long Math Proofs

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

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

ChangBrootalaberdycabhanlistiszipheadWho cares what humans think?

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

pepe2907I 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?

pepe2907And 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.

dtxxTraction 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.

Kedasalfie_nullEasy. 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.

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

scottpeterswayReturnersI disagree.

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

EikkaThat'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.

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

BoniaPlease sign in to add a comment. Registration is free, and takes less than a minute. Read more