Stories
Slash Boxes
Comments

SoylentNews is people

posted by cmn32480 on Wednesday June 01 2016, @12:31AM   Printer-friendly
from the 2+2!=5 dept.

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.

Original Study


Original Submission

 
This discussion has been archived. No new comments can be posted.
Display Options Threshold/Breakthrough Mark All as Read Mark All as Unread
The Fine Print: The following comments are owned by whoever posted them. We are not responsible for them in any way.
  • (Score: 2) by VLM on Wednesday June 01 2016, @12:25PM

    by VLM (445) Subscriber Badge on Wednesday June 01 2016, @12:25PM (#353432)

    But trying to make all of mathematics into a programming language will fail for, oh so many reasons.

    Start with one? Other than the extremely obvious known forklift upgrade issues of "its gonna be expensive and take awhile and be semi-incompatible with the legacy system in funny ways"

    Its not a language syntax problem anyway. Its architectural failings.

    Given a zillion lines of code written in INTERCAL or even worse COBOL, at some point you can't move forward and you can't line by line translate into clojure or something one line at a time, so you have to forklift upgrade the whole thing and re implement the whole system in something more powerful.

    People dislike coq in the same way they dislike r, but they use it anyway. Some unit tests, some abstraction, a couple billion lines of code, we'll have something going on. Super-coq-2.0 sounds like a pr0n movie but is probably whats needed.

    I'd stand by my theory that much like programming eventually there's going to be some problem that can only be solved by a forklift upgrade top to bottom of "math" as a technology. They'll eventually exist some attractive goal, a physics theory of everything, some cryptographic problem, star trek style warp drive, something, and its only going to be solvable with a forklift upgrade of "math" as a pre-req.

    Something that is insightful and worth considering is the new system will be more powerful and capable of really cool things and fit existing knowledge really well, but much like "R" today, it'll still be a steaming pile of WTF. Better doesn't mean easier to learn or more rationally designed, especially if the explicit goal definition of better was to be faster or more capable. Given that R is about the limit of BS that people will tolerate, there might be human limits preventing a system strong enough. Then you'd need an intermediate language, much like AMD64 machine language is a PITA to program effectively in, but compilers take care of that. I wonder how many layers of DSLs and compilers a "math" technology would require to make it human compatible.

    Starting Score:    1  point
    Karma-Bonus Modifier   +1  

    Total Score:   2