Wikipedia-size maths proof too big for humans to check
newscientist.com
Wikipedia-size maths proof too big for humans to check
1–10 of 65 posts
Re: Wikipedia-size maths proof too big for humans to check
#2Re: Wikipedia-size maths proof too big for humans to check
#3Re: Wikipedia-size maths proof too big for humans to check
#4So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem with such a proof satisfying purpose one; I may not be able to check it myself, but I can build a chain of trustworthiness all the way back to a program that I can check myself. In such a chain, the truth of the final result is not, to me, in dispute.
Alas, such a proof throughly fails the second test. I can't see how to gain insight into the problem from such a proof, beyond just it validating previous thought chains of the form "If X were true, then I could deduce Y". It doesn't reveal more about the structure of the problem, or other results in the space.
It's no doubt useful (and all credit to the authors), but in terms of generating new mathematics, I'm dubious. Perhaps people more versed in this specific sub-field can tell me if I'm wrong?
Re: Wikipedia-size maths proof too big for humans to check
#5From the linked Wikipedia article:
> All experiments were conducted on PCs equipped with an Intel Core i5-2500K CPU running at 3.30GHz and 16GB of RAM.
Why are these experiments not being conducted on a more powerful computer or a cluster?
Re: Wikipedia-size maths proof too big for humans to check
#6From the linked Wikipedia article: > All experiments were conducted on PCs equipped with an Intel Core i5-2500K CPU running at 3.30GHz and 16GB of RAM. Why are these experiments not being conducted on a more powerful computer or a cluster?
Because it only took 6 hours anyway.
Re: Wikipedia-size maths proof too big for humans to check
#7So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem with such a proof satisfying purpose one; I may not be able to check it myself, but I can build a chain of trustworthiness all the way back to a program that I can check myself. In such a chain, the truth of the final result is not, to me, in dispute. Alas, such…
It is a field of AI, not a field of Mathematics.
Automated Theorem Proving is a very old field, one of the earliest fields of Artificial Intelligence. The first proof of this nature was the Four Color Theorem, proven by an automated reasoner as opposed to a mathematician.
At which point, the insight into the matter is understanding the AI algorithm and how the AI searches for a solution. And finally... how we can be sure that the AI itself is provably correct.
http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_com...
Re: Wikipedia-size maths proof too big for humans to check
#8So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem with such a proof satisfying purpose one; I may not be able to check it myself, but I can build a chain of trustworthiness all the way back to a program that I can check myself. In such a chain, the truth of the final result is not, to me, in dispute. Alas, such…
It is a field of AI, not a field of Mathematics. Automated Theorem Proving is a very old field, one of the earliest fields of Artificial Intelligence. The first proof of this nature was the Four Color Theorem, proven by an automated reasoner as opposed to a mathematician. At which point, the insight into the matter is understanding the AI algorithm and how the AI searches for a solution. And finally... how we can be…
[deleted]
Re: Wikipedia-size maths proof too big for humans to check
#9So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem with such a proof satisfying purpose one; I may not be able to check it myself, but I can build a chain of trustworthiness all the way back to a program that I can check myself. In such a chain, the truth of the final result is not, to me, in dispute. Alas, such…
I don't claim to be better versed in this field, but a way forward could be to do common subexpression elimination on this proof. Then, try and give names to those common subexpressions.
Finding common subexpressions in such a proof could be a separate field of research. It probably isn't a matter of looking for repeated strings.
Re: Wikipedia-size maths proof too big for humans to check
#10So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem with such a proof satisfying purpose one; I may not be able to check it myself, but I can build a chain of trustworthiness all the way back to a program that I can check myself. In such a chain, the truth of the final result is not, to me, in dispute. Alas, such…
In this case, I don't see why the proof is considered to be the output of the program, but rather the entire program itself. If you can verify the soundness of the software and hardware involved (I certainly can't, but I presume the verification has been done), why should a human need to actually read the output?