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: 2) by looorg on Monday August 24 2020, @09:58AM (7 children)
>My professor would let me fail an exam if I would come up with such answer.
There is a segment of thinking that such "proofs" are not actually proofs at all but merely computations or calculations. Since they can't be verified by other means then the calculations and the solution doesn't usually add any new form of mathematical knowledge. There exists a few such proofs (or solutions) over the years that most seem to be ok with, but as a general way of proving or solving problems they are not I would say well regarded. So indeed, I'm fairly sure I would have been failed to had I just handed in a giant printout of some computation as the solution (it's might be A solution, it just not be THE or ALL solutions) or proof of something.
(Score: 0) by Anonymous Coward on Monday August 24 2020, @11:25AM
The problem with that thinking is that a formal mathematical proof is ultimately just a series of mathematical formulas verified through computation, which is not entirely automate-able but computers actually verify proofs better than humans can. The only difficulty that computers have is in creating proofs, because creating mathematical proofs is NP-complete.
(Score: 3, Insightful) by epitaxial on Monday August 24 2020, @12:37PM (1 child)
I remember thinking geometry class in school would be way more interesting than algebra. Geometry was a terrible class. 90% of it was using proofs to figure out if one line was longer than the other or some nonsense. To this day I still have no idea how to know what proof to use on which problem. Meanwhile I can design shit in SolidWorks all day.
(Score: 2) by looorg on Monday August 24 2020, @03:26PM
I didn't quite enjoy geometry in high school, it felt stupid -- you draw some and then it was usually just computations according to some formula. It wasn't until university and a course in Euclidean Geometry where a lot of those formulas was in some regard explained and/or proven. You don't have to prove it to use it tho, someone did that for you and created a shortcut (the software in question). So it works. Just like a lot of things in life work for most of us, I don't really know exactly how or why but they do and that is good enough in some cases.
(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.
(Score: 1, Insightful) by Anonymous Coward on Monday August 24 2020, @07:34PM
There certainly is, but one only need apply it to any other field of endeavor. to see how ridiculous it is.
Say I make a machined part, with tolerances so fine I could neither make nor measure it with hand tools. But I can make it with one machine, and measure it with another. I'm not entirely sure what the precisely analogous claim is: This is not a real tolerance? That I didn't really make the part? Surely not that it isn't a real part...
Regardless, anyone making any of these candidate claims would be laughed out of the shop.
Making tools to make better tools to accomplish tasks we otherwise couldn't is the essence of human progress; mathematics is no exception, as we build theorems on axioms, then use these theorems to prove that other theorems follow from the same axioms, without "manually" chasing the whole way down to axioms each time. The idea that it somehow loses validity if you can't fit all the tools in your head is precisely as silly as that precision machining is invalid if you can't fit the tools in your hands.
(Score: 2) by FatPhil on Tuesday August 25 2020, @03:13AM
There's a similar fatuous faction in physics - there's no obligation for the laws of the natural world to be elegant. Check out Sabine Hossenfelder's /Lost in Math(s)/ (available in many languages) if you want to see this argument unravelled.
Elegance is nice, but there's no reason its absence implies anything more than non-elegance, certainly nothing about truthiness can be inferred from that property.
Great minds discuss ideas; average minds discuss events; small minds discuss people; the smallest discuss themselves