Computer generated math proof is largest ever at 200 terabytes

May 30, 2016 by Bob Yirka report
Credit: Victorgrigas/Wikideia/ CC BY-SA 3.0

(Phys.org)—A trio of researchers has solved a single math problem by using a supercomputer to grind through over a trillion color combination possibilities, and in the process has generated the largest math proof ever—the text of it is 200 terabytes in size. In their paper uploaded to the preprint server arXiv, Marijn Heule with the University of Texas, Oliver Kullmann with Swansea University and Victor Marek with the University of Kentucky outline the math problem, the means by which a supercomputer was programmed to solve it, and the answer which the proof was asked to provide.

The has been named the boolean Pythagorean Triples problem and was first proposed back in the 1980's by mathematician Ronald Graham. In looking at the Pythagorean formula: a2 + b2 = c2, he asked, was it possible to label each a non-negative integer, either blue or red, such that no set of integers a, b and c were all the same color. He offered a reward of $100 to anyone who could solve the problem.

To solve this problem the researchers applied the Cube-and-Conquer paradigm, which is a hybrid of the SAT method for hard problems. It uses both look-ahead techniques and CDCL solvers. They also did some of the math on their own ahead of giving it over to the computer, by using several techniques to pare down the number of choices the would have to check, down to just one trillion (from 102,300). Still the 800 processor supercomputer ran for two days to crunch its way through to a solution. After all its work, and spitting out the huge data file, the computer proof showed that yes, it was possible to color the integers in multiple allowable ways—but only up to 7,824—after that point, the answer became no.

While technically, the team, along with their computer did create a proof for the problem, questions remain, the first of which is, is the proof really a proof if it does not answer why there is a cut-off point at 7,825, or even why the first stretch is possible? Strictly speaking, it is, the team used another computer program to verify the results, and the proof did give a definitive answer to the original question—which caused Graham to make good on his offer by handing over the $100 to the research team—but, nobody can read the proof (or other similar but smaller proofs also generated by computers but which are still too large for a human to read) which begs the philosophical question, does it really exist?

Explore further: Computer generated math proof is too large for humans to check

More information: Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer, arXiv:1605.00723 [cs.DM] arxiv.org/abs/1605.00723

Abstract
The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set N = {1,2,...} of natural numbers be divided into two parts, such that no part contains a triple (a,b,c) with a2+b2=c2 ? A prize for the solution was offered by Ronald Graham over two decades ago.
We solve this problem, proving in fact the impossibility, by using the Cube-and-Conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days.
Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking.

via Nature

Related Stories

Blog comment, collab help man attack old maths problem

September 26, 2015

Chris Cesare in Nature reported on Friday that Terence Tao successfully attacked the Erdős discrepancy problem by building on an online collaboration. Tao is a professor in the math department at UCLA. He works primarily ...

Recommended for you

How to cut your lawn for grasshoppers

November 22, 2017

Picture a grasshopper landing randomly on a lawn of fixed area. If it then jumps a certain distance in a random direction, what shape should the lawn be to maximise the chance that the grasshopper stays on the lawn after ...

Plague likely a Stone Age arrival to central Europe

November 22, 2017

A team of researchers led by scientists at the Max Planck Institute for the Science of Human History has sequenced the first six European genomes of the plague-causing bacterium Yersinia pestis dating from the Late Neolithic ...

Ancient barley took high road to China

November 21, 2017

First domesticated 10,000 years ago in the Fertile Crescent of the Middle East, wheat and barley took vastly different routes to China, with barley switching from a winter to both a winter and summer crop during a thousand-year ...

7 comments

Adjust slider to filter visible comments by rank

Display comments: newest first

mutant456
1 / 5 (8) May 30, 2016
This is good new math research show will and thinkthunk
VINDOC
2 / 5 (8) May 30, 2016
Is this really a good uses of a supercomputer? Why not cure Cancer or Alzheimer's, or Parkinson's disease.
shavera
4.7 / 5 (12) May 30, 2016
^ Dear supercomputer, please solve disease. Thanks.

I'm sure it's just as simple as that.
torbjorn_b_g_larsson
4 / 5 (4) May 30, 2016
So an empirical proof exist and can be checked different way - and philosophy can ask of its existence? Philosophy is not only as meaningless as it seemed, it is ridiculous.
torbjorn_b_g_larsson
3.5 / 5 (6) May 30, 2016
The same utterly stupid and boring trolling phrase: 'Is X really a good use of Y? Why not do Z?''

Is that really good use of comment time? Why not do something constructive, like boning up on False dilemma while learning how to refrain from trolling at the same time? https://en.wikipe..._dilemma

[Or if it isn't obvious, supercomputers are used for both math proofs and, more frequently in fact, to study diseases. There are even math proofs that are used in models of diseases - science (and math) is mutually supportive - but that interesting fact would likely blow a troll's boring mind ...]
eachus
1 / 5 (2) May 30, 2016
The fact that this proof is ridiculously large is just laziness. There is a set of integers less than or including 7824, that cannot be partitioned. Much smaller than 68 gigabytes or the ridiculous 200 terabyte exposition. It takes less than 32k bytes to list that set. The proof then shows that 7825 cannot be added to the set. (Of course, calling it laziness does not reflect the CPU time required to strip out those values are unnecessary. That might take years of CPU time. ;-)
Emptycell
4.2 / 5 (5) May 30, 2016
The comment about wasting money that could be better spent is just the same old fallacy trotted, that was used against NASA. They never mention the fact that every dollar spent on the space race earned the USA at least 100 in return.

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

Click here to reset your password.
Sign in to get notified via email when new comments are made.