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, Insightful) by Anonymous Coward on Wednesday June 01 2016, @01:11AM

    by Anonymous Coward on Wednesday June 01 2016, @01:11AM (#353292)

    That just shows you are an uneducated math-illiterate fool.

    Testing all possible combinations to reach a conclusion is a valid proof technique.

    Starting Score:    0  points
    Moderation   +2  
       Insightful=1, Informative=1, Total=2
    Extra 'Insightful' Modifier   0  

    Total Score:   2  
  • (Score: 0) by Anonymous Coward on Wednesday June 01 2016, @01:29AM

    by Anonymous Coward on Wednesday June 01 2016, @01:29AM (#353298)

    Testing all possible combinations to reach a conclusion is a valid proof technique.

    It is. It just isn't elegant. Also it opens up that horrible problem of how do you know that you, or they, tested all the possible combinations. The main problem here is that I doubt many, or any, would want to check a 200 Terabyte datadump. How will we know ...

    • (Score: 3, Insightful) by bzipitidoo on Wednesday June 01 2016, @01:44AM

      by bzipitidoo (4388) on Wednesday June 01 2016, @01:44AM (#353302) Journal

      Not elegant? Get used to it. So called "computer proofs", in which computers exhaustively check all of a huge but not infinite number of possibilities, have been around for years now.

      We'd all like to see Fermat's proof that wouldn't quite fit in the margins of a single page, love to see mathematical induction reduce infinity to less than a dozen special cases, swoon over a one page proof that P != NP, and faint with joy and amazement over a hundred page Theory of Everything. But I'll take massive petabyte sized proofs any time over no proof at all.

      • (Score: 2) by edIII on Wednesday June 01 2016, @07:49PM

        by edIII (791) on Wednesday June 01 2016, @07:49PM (#353628)

        I might get used to a lack of elegance. That is rather subjective in many cases. However, I can't get around the fact the proof is about as useful as tits on a bull. Moreover, I don't consider that 200TB to be proof of anything intrinsically. Where is the logic? Where is the mind bending math I need to decipher?

        But I'll take massive petabyte sized proofs any time over no proof at all

        That's not as elegant as providing the all of the code and documented logic that produced this "proof". If all you have is the programmatic output of brute force checking of permutations then the output is nearly useless as proof. The lines of code are the proof themselves, not the output. If you wanted to prove the output was "proof", or peer review it as it were, you would need to write more code again.

        So that 200TB is meaningless unless accompanied by the code, which raises the question then, of why include the entire 200TB anyways? You could include a GB of it or so to be spot checked by the program. If the logic of the code is sound and capable of passing multiple peer reviews, than we truly don't need to be hauling around that 200TB do we?

        I don't carry around 4 billion numbers with me every day, but just have confidence I can generate them on demand ;)

        --
        Technically, lunchtime is at any moment. It's just a wave function.
    • (Score: 2) by darkfeline on Wednesday June 01 2016, @03:15AM

      by darkfeline (1030) on Wednesday June 01 2016, @03:15AM (#353324) Homepage

      Reality isn't elegant. Best get used to it now.

      --
      Join the SDF Public Access UNIX System today!
      • (Score: 0) by Anonymous Coward on Wednesday June 01 2016, @04:37PM

        by Anonymous Coward on Wednesday June 01 2016, @04:37PM (#353530)

        And this proof is far more elegant than 10^2300-ish lines of the form saying "colouring X_i is invalid because PPT a, b, and c are the same colour".

    • (Score: 4, Insightful) by q.kontinuum on Wednesday June 01 2016, @04:42AM

      by q.kontinuum (532) on Wednesday June 01 2016, @04:42AM (#353341) Journal

      No one has to go through all the data. Go through the source code, prove it's correctness and run it yourself. It's a kind of meta-evaluation, and seen that way the poof is much more elegant / appealing.

      --
      Registered IRC nick on chat.soylentnews.org: qkontinuum
      • (Score: 0) by Anonymous Coward on Wednesday June 01 2016, @10:11AM

        by Anonymous Coward on Wednesday June 01 2016, @10:11AM (#353401)

        Something something about not being able to run this program in MS/DOS mode...