Interesting. I hope what the author says isn't actually done. So the computers generated a proof nobody can understand, but fret not, a second computer program can assure us of its validity. Well that's heartwarming. I hope they are not building the foundations of future math on this house of cards.
If you think a shorter elegant proof is more desirable, well, I totally agree with you. I think math is more about the proofs than the results. On the other hand I have zero problems trusting a proof checked by a computer. I don't know you but I usually trust much more computers with tedious computations than myself.
> fret not, a second computer program can assure us of its validity
Formal methods are rigorous enough and mature enough to be helpful in avionics software development, why not in research mathematics?
> I hope they are not building the foundations of future math on this house of cards.
Mathematics is always a house of cards, and human mathematicians will always be fallible. It's already possible for a published result to later turn out to be invalid, in turn invalidating papers that relied on it.
How about: a group of highly sophisticated and very skilled mathematicians generate a proof no mere mortals (and lesser mathematicians) can understand, but fret not: another genius mathematician can assure us of its validity.
Hmmmmmmm. Yeah, that sounds much better. What do you think?
I guess the problem with many Computer Assisted Proofs is that they don't explain "why" something is true, only that something is true. But if that's the best you can do, then it's certainly better than nothing.
Also, advances in CAPs can have applications outside of pure maths.
Finally, CAPs are not common enough - or viable enough in most cases - to make a dent in the practice of pure maths. At least that's the impression I get.
The article explains that the translation from the original problem to the computer-checked problem was quite ingenious.
Turning a problem about continuous space to a graph problem, and then using a computer to check the graph problem does not kill much (or any) of the art form I would think.
I think one could only claim destruction if there was evidence that other forms of math were in decline due to computer-aided proofs.
As much as we hear about computer-aided proofs and theorem proving software here on HN, these topics are still somewhat niche in mathematics as a whole.
I brushed up against SAT solvers in school, but never quite got a grasp on them. The "proof" at the end is 200 GB - is that size related to SAT solvers in general, this particular problem, the dimensionality here? A billion-sized search space giving a 1.6 trillion bit proof sounds awfully exhaustive to me, but I also can't imagine what such a large proof would even be about.
If you're talking about boolean satisfiability, all you have as "memory locations" are bits and you describe their relationships. I guess the result you want is "unsat".
Say you want location 1 not equal location 2, then you have
(1 or 2) and (not 1 and not 2) in the expected normal form. This blows up fast if multiple variables are involved. There are tricks like Tseitin transformation that can reduce the size of the clauses but introduces additional variables.
Also, if you want to use 8-bit-numbers, you'd need 8 variables each. Addition would need more clauses.
The four color theorem was proven with the help of a computer in 1976 [0]. The event gave rise to the concept of non-surveyable proof [1]. As far as I can tell, it has never been proven without the help of a computer.
As the Wikipedia article states, the main countermeasure to non-surveyability is to express the proof in formal logic, which can then be verified by an automated proof checker. In fact, this is exactly what the authors of the proof of Keller's conjecture have done. And likewise, the Four Colour Theorem has been verified in this way.
I don't think non-surveyability is really the issue here.
Non-surveyability was introduced precisely as a criticism of the 1976 proof. I believe that the four color theorem was proven with the help of an automated proof checker only in 2005.
Don't forget the kicker: the original computer-powered proof turned out to to have several serious flaws, brought to light after work done by several researchers unconnected to the original effort. ctrl-f for Schmidt.
I had to search the original publication to see what kind of computer cluster they used. Here it is in case you are curious:
"We ran all three experiments simultaneously on 20 nodes on the Lonestar5 cluster and computing on 24 CPUs per node in parallel."
It seems it took less than an hour. I think that calling it a "fleet of computers" is a little too much. It makes it look like they brute-forced the problem while the truth is that as usually the merit was on the algorithm.
Am I the only one wondering why they used 40 computers, if the computation only lasted for 30 minutes? Does anyone who read the full paper jnow the reason? The article does not explain anything in that direction, but I would expect that if they could just do it on one computer and wait for two days, they would have done it...
Skimming it the answer appears to be “because they had that cluster”. They say they only used 20 machines (each with 24 CPUs, so I guess these are fairly beefy)
Given the 224 GB (binary) size of the proof memory usage might be a problem, too.
23 comments
[ 2.6 ms ] story [ 65.7 ms ] threadIf you think a shorter elegant proof is more desirable, well, I totally agree with you. I think math is more about the proofs than the results. On the other hand I have zero problems trusting a proof checked by a computer. I don't know you but I usually trust much more computers with tedious computations than myself.
Formal methods are rigorous enough and mature enough to be helpful in avionics software development, why not in research mathematics?
> I hope they are not building the foundations of future math on this house of cards.
Mathematics is always a house of cards, and human mathematicians will always be fallible. It's already possible for a published result to later turn out to be invalid, in turn invalidating papers that relied on it.
Hmmmmmmm. Yeah, that sounds much better. What do you think?
Also, advances in CAPs can have applications outside of pure maths.
Finally, CAPs are not common enough - or viable enough in most cases - to make a dent in the practice of pure maths. At least that's the impression I get.
Edit: typo
Turning a problem about continuous space to a graph problem, and then using a computer to check the graph problem does not kill much (or any) of the art form I would think.
As much as we hear about computer-aided proofs and theorem proving software here on HN, these topics are still somewhat niche in mathematics as a whole.
Say you want location 1 not equal location 2, then you have
(1 or 2) and (not 1 and not 2) in the expected normal form. This blows up fast if multiple variables are involved. There are tricks like Tseitin transformation that can reduce the size of the clauses but introduces additional variables.
Also, if you want to use 8-bit-numbers, you'd need 8 variables each. Addition would need more clauses.
[0] https://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_co... [1] https://en.wikipedia.org/wiki/Non-surveyable_proof
I don't think non-surveyability is really the issue here.
"We ran all three experiments simultaneously on 20 nodes on the Lonestar5 cluster and computing on 24 CPUs per node in parallel."
It seems it took less than an hour. I think that calling it a "fleet of computers" is a little too much. It makes it look like they brute-forced the problem while the truth is that as usually the merit was on the algorithm.
Skimming it the answer appears to be “because they had that cluster”. They say they only used 20 machines (each with 24 CPUs, so I guess these are fairly beefy)
Given the 224 GB (binary) size of the proof memory usage might be a problem, too.