SoylentNews is people
SoylentNews
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.
(Score: 0) by Anonymous Coward on Monday August 24 2020, @01:42PM (1 child)
I disagree. This method of proof has been around for quite some time and works well. It is only recently (relatively speaking) that it can be used for much larger scale problems. Previously this method was limited by the number of cases that could be verified. The issue is not the computation but in the reduction of the original problem to a new, iterable problem space. This is what I would consider to be the actual "proof". As long as you can demonstrate that the original problem can be reduced to a finite set of cases that can then be solved/tested then it should be acceptable. Anyone should be able to repeat/verify the calculation but the calculation only proves the original hypothesis if the reduction is correct.
(Score: 2) by looorg on Monday August 24 2020, @03:21PM
Good for you. It has been around for quite some time, and used for quite some time. On of those computational proofs everyone is ok with would be the four-color theorem (1976? or there about). That isn't to say that it's liked by all, one common critique tends to be that they lack what is sometimes referred to as mathematical elegance or simplicity. Calculations are just not considered to be elegant in that regard, beyond that the common complaint as I recall it is that they usually offer a solution but quite possibly not all solutions. In which case it's not considered a complete proof.