5 ms·

A fleet of computers helps settle a 90-year-old math problem

40 points by doppp 6y ago

ars 6y ago
Original source: https://www.quantamagazine.org/computer-search-settles-90-year-old-math-problem-20200819/ https://www.quantamagazine.org/computer-search-settles-90-ye...
- acqq 6y ago
  The author of both articles is the same, as far as I understand, so I don’t understand how one article can be “more original source” than another.
  - azepoi 6y ago
    The other article was discussed here: https://news.ycombinator.com/item?id=24220149 https://news.ycombinator.com/item?id=24220149
marta_morena_25 6y ago
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.
- plafl 6y ago
  I don't share your pessimism. 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.
- MaxBarraclough 6y ago
  > 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.
- throwaway_pdp09 6y ago
  Perhaps you can offer something better?
  - Joker_vD 6y ago
    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?
smabie 6y ago
For math as an art form (a lot of theoretical math), are computer aided proofs destroying the core value of the endeavor?
- ogogmad 6y ago
  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.
- throwaway_pdp09 6y ago
  I guess if a human can't do it and a computer can, then no, it's not. What would be the other side to that argument?
- plafl 6y ago
  I think the art is moved from the proof itself to translating the proof to computer language. Edit: typo
- FartyMcFarter 6y ago
  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.
- kevinventullo 6y ago
  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.
hirsin 6y ago
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.
- maweki 6y ago
  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.
isolli 6y ago
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. [0] https://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer https://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_co... [1] https://en.wikipedia.org/wiki/Non-surveyable_proof https://en.wikipedia.org/wiki/Non-surveyable_proof
- ogogmad 6y ago
  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.
  - isolli 6y ago
    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.
- MaxBarraclough 6y ago
  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.
plafl 6y ago
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.
tduberne 6y ago
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...
- Someone 6y ago
  Paper is at https://arxiv.org/abs/1910.03740 https://arxiv.org/abs/1910.03740. 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.

40 points by doppp 6y ago

ars 6y ago

Original source: https://www.quantamagazine.org/computer-search-settles-90-year-old-math-problem-20200819/ https://www.quantamagazine.org/computer-search-settles-90-ye...

acqq 6y ago
The author of both articles is the same, as far as I understand, so I don’t understand how one article can be “more original source” than another.
- azepoi 6y ago
  The other article was discussed here: https://news.ycombinator.com/item?id=24220149 https://news.ycombinator.com/item?id=24220149

marta_morena_25 6y ago

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.

plafl 6y ago
I don't share your pessimism. 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.
MaxBarraclough 6y ago
> 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.
throwaway_pdp09 6y ago
Perhaps you can offer something better?
- Joker_vD 6y ago
  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?

smabie 6y ago

For math as an art form (a lot of theoretical math), are computer aided proofs destroying the core value of the endeavor?

ogogmad 6y ago
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.
throwaway_pdp09 6y ago
I guess if a human can't do it and a computer can, then no, it's not. What would be the other side to that argument?
plafl 6y ago
I think the art is moved from the proof itself to translating the proof to computer language. Edit: typo
FartyMcFarter 6y ago
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.
kevinventullo 6y ago
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.

hirsin 6y ago

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.

maweki 6y ago
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.

isolli 6y ago

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. [0] https://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer https://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_co... [1] https://en.wikipedia.org/wiki/Non-surveyable_proof https://en.wikipedia.org/wiki/Non-surveyable_proof

ogogmad 6y ago
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.
- isolli 6y ago
  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.
MaxBarraclough 6y ago
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.

plafl 6y ago

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.

tduberne 6y ago

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...

Someone 6y ago
Paper is at https://arxiv.org/abs/1910.03740 https://arxiv.org/abs/1910.03740. 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.