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: 4, Insightful) by wisnoskij on Wednesday June 01 2016, @01:58AM
Considering that it is making a prediction against all non-negative integers, aka infinity, this cannot be the output of all possible solutions. There is nothing in Math that says that all provable concepts can be proven elegantly. In fact many things simply cannot be proven, and for all elegant proofs I would be willing to bet that their exist many many more problems where the absolutely smallest proof is many millions of lines long or longer. Unfortunately, this is probably where Math will be heading fast. All the worthwhile man-provable things will run out, and Math will be be almost exclusively dealing with proofs that cannot ever be checked by hand or understood by beings unable to do many billions of calculations per second. It will simply be a matter of programming computers to solve problems and assuming that if that programming is correct the output probably is as well.
(Score: 2) by mhajicek on Wednesday June 01 2016, @02:55AM
Did you RTFS?
"it was possible to color the integers in multiple allowable ways—but only up to 7,824—after that point, the answer became no."
They didn't go to infinity. They had the machine check one trillion cases.
The spacelike surfaces of time foliations can have a cusp at the surface of discontinuity. - P. Hajicek
(Score: -1, Troll) by Anonymous Coward on Wednesday June 01 2016, @04:27AM
So it prove it is 7,824. Ok, do it. Prove it was not a bug in the code. I can always prove a bug, but NOT bug-free.
Now read "The Nine Billion Names of God", and real understand the question.
(Score: 2) by q.kontinuum on Wednesday June 01 2016, @04:48AM
Software correctness can be formally proven. However, this doesn't account for bit-flips due to radiation or faulty hardware...
Registered IRC nick on chat.soylentnews.org: qkontinuum
(Score: 0) by Anonymous Coward on Wednesday June 01 2016, @06:24PM
Not really. Software correctness can have a strong backing but prove to be bug-free. Even a single assembler ops (an atom) can still be broken by a bug... Cold solder joint, heating, bit-flip, error in microcode (quarks) , even physical bug.
So to the base question 200TB "proof". It is a listing not a proof.
(Score: 2) by q.kontinuum on Thursday June 02 2016, @06:39AM
A bit-flip is not a bug in software, it is faulty hardware (as I mentioned before). Correctness of the software: The first article I found [wikipedia.org] is about correctness of the algorithm. To prove correctness of the source code, next step would be to include the behaviour of the compiler for the specific architecture (word-length, if applicable rounding for floats, etc.) Should still be possible to prove correctness.
It probably gets impractical if you need to prove the correctness of the compiler as well (unless software was coded in assembler, in which case the correctness of the implementation will be harder to prove). For the execution, I would expect that only statistical statements are possible, as in "The proof is valid within x sigma" due to potential bugs. The chances can be increased by redundant hardware and error-checking, and considering that our all lives depends on reliability of some computer-controlled nuclear missile launchers, I would expect that for all practical purposes the risk of accepting a wrong evidence in maths is less than the risk of being wiped out due to a computer error.
Registered IRC nick on chat.soylentnews.org: qkontinuum
(Score: 2) by VLM on Wednesday June 01 2016, @12:36PM
The problem is there's an infinite set of proofs where the "termination point" or "last time it worked" is a smooth white noise distribution of numbers between zero and infinity.
So that's my mental model I can imagine in my mind of all of "proof space". This situation is one specific problem with a tiny little dot at 7824 cases.
The problem is there's an infinite number of math proofs, which are presumably just as interesting as this one to some weirdo out there, that don't terminate until some ridiculously large Ackermann function value that'll never be computed.
Essentially you're claiming that the existence of one program that rapidly-ish halts proves the Turing halting problem doesn't exist as a general problem.