SoylentNews is people
SoylentNews
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 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: 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 supercomputer 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.
(Score: 2) by Non Sequor on Wednesday June 01 2016, @01:51AM
Almost all of the real numbers can't be described by any finite program. These numbers exist by implication of the procedure used to take the algebraic closure of the rational numbers combined with your basic arithmetic operations, but they're effectively unnameable. In practice, we can only use computable numbers. These are numbers that can be generated (up to a parameterized precision) by a finite program using a tractable algorithm. These are the numbers that can be conceivably given names. But again, if you impose resource constraints on the programs (code size less than x, execution time less than y), you drop down to an even smaller set of numbers we can give names using bounded resources. And yet again, if you look at the resources that will be available over all of human existence and ask how much resources can be invested in computation, then you drop down to an even smaller set of numbers that will be named by mankind.
A specific example of this progression is GUIDs. 128 fair coin flips gives you a sequence of bits that has a negligible chance of being generated twice under current usage levels, and it's not that hard to expand the ID space to make it implausible that the same sequence will be generated twice in the history of the universe. We have linguistic constructions to give names to what we regard as very large integers, or very large spans of decimal digits, but most of these names will never be uttered by human lips.
Now against all this, I have to wonder if a 200TB proof is large or if it's merely a quaint human artifact? One might imagine that, if human intuition can lead us to conjectures then perhaps there is a bound on the required proof size since generally a conjecture implies the existence of a proof (either for or against) with some steps not fully filled in. Or, maybe there isn't a relationship between the things that we can speculate on and the resources needed to resolve this speculation.
Write your congressman. Tell him he sucks.
(Score: 0) by Anonymous Coward on Wednesday June 01 2016, @03:29AM
Not quite: there are real numbers that can be named and reasoned about which are not computable. Such numbers can be constructed them using, for example, known non-computable functions such as the busy beaver function. These numbers are called definable. But it is still the case that almost all real numbers are not definable, as there are uncountably many reals and only a countable subset of them are definable.
(Score: 2) by Non Sequor on Wednesday June 01 2016, @03:47AM
I know and I'd argue that the actual concrete values of things which are definable but not computable actually do not figure significantly in their use. These are objects with no realizable construction.
Write your congressman. Tell him he sucks.
(Score: 0) by Anonymous Coward on Wednesday June 01 2016, @09:48AM
(a + b)(c - d) = e
e = ac + bc - ad - bd
I wrote a basic program to do that kind of algebraic manipulation on a Vic-20
Tell me again how supercomputers can't deal with real numbers?