Stories
Slash Boxes
Comments

SoylentNews is people

posted by Fnord666 on Monday August 24 2020, @08:57AM   Printer-friendly
from the now-that-that's-settled dept.

A Fleet of Computers Helps Settle a 90-Year-Old Math Problem:

A team of mathematicians has finally finished off Keller's conjecture, but not by working it out themselves. Instead, they taught a fleet of computers to do it for them.

Keller's conjecture, posed 90 years ago by Ott-Heinrich Keller, is a problem about covering spaces with identical tiles. It asserts that if you cover a two-dimensional space with two-dimensional square tiles, at least two of the tiles must share an edge. It makes the same prediction for spaces of every dimension—that in covering, say, 12-dimensional space using 12-dimensional "square" tiles, you will end up with at least two tiles that abut each other exactly.

Over the years, mathematicians have chipped away at the conjecture, proving it true for some dimensions and false for others. As of this past fall, the question remained unresolved only for seven-dimensional space.

But a new computer-generated proof has finally resolved the problem. The proof, posted online last October, is the latest example of how human ingenuity, combined with raw computing power, can answer some of the most vexing problems in mathematics.

The authors of the new work—Joshua Brakensiek of Stanford University, Marijn Heule and John Mackey of Carnegie Mellon University, and David Narváez of the Rochester Institute of Technology—solved the problem using 40 computers. After a mere 30 minutes, the machines produced a one-word answer: Yes, the conjecture is true in seven dimensions. And we don't have to take their conclusion on faith.

The answer comes packaged with a long proof explaining why it's right. The argument is too sprawling to be understood by human beings, but it can be verified by a separate computer program as correct.

In other words, even if we don't know what the computers did to solve Keller's conjecture, we can assure ourselves they did it correctly.


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: 0) by Anonymous Coward on Monday August 24 2020, @12:44PM (7 children)

    by Anonymous Coward on Monday August 24 2020, @12:44PM (#1041109)

    how is the verifying program verified?

  • (Score: 4, Informative) by maxwell demon on Monday August 24 2020, @01:12PM (2 children)

    by maxwell demon (1608) on Monday August 24 2020, @01:12PM (#1041116) Journal

    I guess the algorithm is simple enough for a human to understand it, and therefore to verify that it does indeed do what it is intended to do.

    Of course there's always the possibility of compiler bugs, but then, having an independent program checking it makes it very unlikely to hit a set of bugs that makes the verifying program to falsely pass the wrong proof that the generating program generated is sufficiently unlikely.

    Of course there's also the possibility that the program has a bug that the humans have not spotted, but then, there's also the possibility that a hand-written proof has an error that nobody spotted.

    --
    The Tao of math: The numbers you can count are not the real numbers.
    • (Score: 1, Interesting) by Anonymous Coward on Monday August 24 2020, @01:55PM (1 child)

      by Anonymous Coward on Monday August 24 2020, @01:55PM (#1041129)

      I guess the algorithm is simple enough for a human to understand it, and therefore to verify that it does indeed do what it is intended to do.

      Of course there's always the possibility of compiler bugs, but then, having an independent program checking it makes it very unlikely to hit a set of bugs that makes the verifying program to falsely pass the wrong proof that the generating program generated is sufficiently unlikely.

      Of course there's also the possibility that the program has a bug that the humans have not spotted, but then, there's also the possibility that a hand-written proof has an error that nobody spotted.

      Whenever I've seen a proof like this fail, it's been in the initial reduction of the hypothesis to the simplified problem space that they verify by brute force.

      The strong form of this proof is

      1. A is true if and only if B is true.
      2. Prove B is true, thus proving A is true as well or
      3. Prove B is false, thus proving A is false as well.

      In cases like this B is proven by iterating over all of the possible cases of B. The weak link is the "if and only if" part. If that's not completely correct then the computation doesn't matter one iota.

      • (Score: 0) by Anonymous Coward on Monday August 24 2020, @08:04PM

        by Anonymous Coward on Monday August 24 2020, @08:04PM (#1041309)

        Whenever I've seen a proof like this fail, it's been in the initial reduction of the hypothesis to the simplified problem space that they verify by brute force.

        So what you're saying is: Sometimes we find mistakes in the part that a human can follow and check for mistakes.
        But whatever mistakes may or may not be lurking in the opaque, machines-only parts, us humans haven't found them yet.

        And no, I'm not suggesting our computers are engaged in a conspiracy of lies; that would be silly. But you have to wonder about aliens with precision cosmic-ray tech flipping bits to stymie our mathematical progress and keep us from developing the warp drive.

  • (Score: 1, Touché) by Anonymous Coward on Monday August 24 2020, @01:29PM

    by Anonymous Coward on Monday August 24 2020, @01:29PM (#1041119)

    how is the verifying program verified?

    With a verification program verifier of course.

  • (Score: 2) by hendrikboom on Monday August 24 2020, @02:58PM (2 children)

    by hendrikboom (1125) Subscriber Badge on Monday August 24 2020, @02:58PM (#1041141) Homepage Journal

    With another verifying program.

    It's feasible to verify that a verifying program indeed follows the rules of the logic it was designed to follow.
    It's even possible for a verifying program to verify that it itself does this.

    BUT:

    It is not in general feasible to verify that the logic is consistent and that the rules are the correct ones for the problem. (says Godel)

    • (Score: 0) by Anonymous Coward on Monday August 24 2020, @11:29PM

      by Anonymous Coward on Monday August 24 2020, @11:29PM (#1041388)

      True, but the domain of verifying mathematical proofs has a general solution, otherwise general purpose automated proof verifiers could not exist. What does not exist is a general method of creating such proofs.

    • (Score: 0) by Anonymous Coward on Monday September 21 2020, @09:07PM

      by Anonymous Coward on Monday September 21 2020, @09:07PM (#1054626)

      Godel didn't say that. In fact, he proved the opposite for Predicate Calculus as Post before him had done for Propositional Calculus. We probably wouldn't have the incompleteness theorem in its current form or at all, if he hadn't done so in his completeness theorem.