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

(—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]

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

Archaeologists discover Cornish barrow site

April 20, 2018

An Archaeologist at The Australian National University (ANU) has discovered a prehistoric Bronze-Age barrow, or burial mound, on a hill in Cornwall and is about to start excavating the untouched site which overlooks the English ...

New ancestor of modern sea turtles found in Alabama

April 18, 2018

A sea turtle discovered in Alabama is a new species from the Late Cretaceous epoch, according to a study published April 18, 2018 in the open-access journal PLOS ONE by Drew Gentry from the University of Alabama at Birmingham, ...

New study improves 'crowd wisdom' estimates

April 18, 2018

In 1907, a statistician named Francis Galton recorded the entries from a weight-judging competition as people guessed the weight of an ox. Galton analyzed hundreds of estimates and found that while individual guesses varied ...


Adjust slider to filter visible comments by rank

Display comments: newest first

1 / 5 (8) May 30, 2016
This is good new math research show will and thinkthunk
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.
4.7 / 5 (12) May 30, 2016
^ Dear supercomputer, please solve disease. Thanks.

I'm sure it's just as simple as that.
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.
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 ...]
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. ;-)
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.