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: 1) by TheSage on Wednesday June 01 2016, @07:16AM

    by TheSage (133) on Wednesday June 01 2016, @07:16AM (#353360) Journal

    You sound quite bitter.

    You give a nice example of judging one field of science/technology with the criteria of another field. The result is not surprising. Rest assured there are good reasons why mathematicians do things the way they do them; for example a big one you have missed is, that a mathematical idea (i.e. the content) is much more important than the way it is formulated (i.e. the way it is written down). Can some aspects of how we do mathematics be improved? Of course they can. But trying to make all of mathematics into a programming language will fail for, oh so many reasons.

    Having said that, it would be an interesting program to pursue; it could provide a new perspective to some fields.

  • (Score: 1, Insightful) by Anonymous Coward on Wednesday June 01 2016, @07:26AM

    by Anonymous Coward on Wednesday June 01 2016, @07:26AM (#353366)

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

    The great Mathematician and Computer Scientist Alan Turing proved this statement wrong with a mathematical proof that is also a computer.

    • (Score: 1) by TheSage on Wednesday June 01 2016, @08:58AM

      by TheSage (133) on Wednesday June 01 2016, @08:58AM (#353380) Journal

      I am not talking here about the theoretical possibility of transforming mathematics into programs. Obviously, this can be done (with the possible exception of some highly meta stuff, depending on what you call mathematics). As should be clear from context, I was talking about the practicality of such an approach. It would be like trying to do biology using only the language of physics (or vice versa). Theoretically possible, but useful only in a very restricted set of problems.

  • (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.