May 30, 2016 report

# Computer generated math proof is largest ever at 200 terabytes

*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 math problem 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: a^{2} + b^{2} = c^{2}, 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 supercomputer would have to check, down to just one trillion (from 10^{2,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

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

© 2016 Phys.org

**Citation**: Computer generated math proof is largest ever at 200 terabytes (2016, May 30) retrieved 25 April 2019 from https://phys.org/news/2016-05-math-proof-largest-terabytes.html

## User comments

mutant456VINDOCshaveraI'm sure it's just as simple as that.

torbjorn_b_g_larssontorbjorn_b_g_larssonIs 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 ...]

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