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: 3, Insightful) by KritonK on Monday August 24 2020, @09:24AM (4 children)
Why not 20 hours on one computer? This doesn't sound like a lot and, unless the algorithm they used is embarrasingly parallel [wikipedia.org], it would have saved them a lot of development time, possibly more than the 19.5 hours they gained from running the parallel version. They would have saved a bit of money, too, if they bought those 40 computers specifically for this purpose. The single-processor version might even be a bit easier to understand.
(Score: 4, Informative) by isj on Monday August 24 2020, @10:04AM
They transformed the problem into a SAT problem with 39.000 variables and fed it into a specialized SAT-solver. Until it finished they probably had no idea how long it would take.
Modern SAT-solvers don't try all 2^39000 combinations. Instead, they cut off search paths as they go along. But you don't know how much can be quickly eliminated until you try.
(Score: 4, Funny) by RamiK on Monday August 24 2020, @10:06AM (2 children)
Cause they have a CS "lab" full of desktops no one uses during the lockdown and spare time to code as the students just watch old lecture recordings and have short 30min Zoom Q&A sessions.
There were other suggestions on the table like bitcoin mining or having Amazon use them for package storage... My personal favorite was to convert the lecture halls into quarantine bed & breakfasts and the labs into non-stop LAN parties instead of a swimming pool for that extra star... Unfortunately, Carol was on the helpdesk and kept repeating "computer says no" and when they had the CS guys try to fix it they ended up using them for this bit of silliness.
compiling...
(Score: 0) by Anonymous Coward on Monday August 24 2020, @01:37PM (1 child)
Perhaps they should have used those computers for day trading on instead.
(Score: 3, Informative) by kazzie on Tuesday August 25 2020, @08:38AM
I'll gladly trade the day I'm having: it's been rubbish.