21–30 of 65 posts
"Wikipedia-sized" Is it really? They say in the article that the text of Wikipedia is a 10GB download, but that has to be compressed (and compression on plaintext, which comprises most of Wikipedia, is extremely efficient). I'm guessing (but have no proof) that their 13GB file was raw data. A minor thing, but comparisons like this always drive me nuts. Just say "13GB proof too big for humans to check." Then there's n…
So, 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…
Earlier quoted context omitted.
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.
I've re-drafted this several times and it always seems to come out snarky. Please believe me that it's not intended as such - my field is mathematics, not English. So please accept this at face value. I have some expertise in this field. My PhD is in combinatorics, which is closely related, and one of the main results used computer search. More, it's closely related to the Four Colour Theorem. To me, what you say mak…
The way I read it, he was suggesting a possible way of reducing the size of the DRUP certificate from 13GByte by searching for common patterns, perhaps similar to the way bzip works.
Earlier quoted context omitted.
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?
Because the output of the program is effectively a long list of cases of things that have been considered[0], and why they do or don't "work" in some sense. The output is independent of the program and, in principle, can be checked. In some ways it's like printing the search tree of chess to show that white has a forced win. It doesn't matter if the program is "correct" - you can check the output separately. [0] EDIT…
"Wikipedia-sized" Is it really? They say in the article that the text of Wikipedia is a 10GB download, but that has to be compressed (and compression on plaintext, which comprises most of Wikipedia, is extremely efficient). I'm guessing (but have no proof) that their 13GB file was raw data. A minor thing, but comparisons like this always drive me nuts. Just say "13GB proof too big for humans to check." Then there's n…
So is OGR-27 merely 27 numbers aka a 1-d pixel "graph" probably around five hundred something pixels, or is it really zillions of gigs of rulers all of which are longer than the OGR?
So, 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…
Imagine if we could program a computer with all known mathematical truths. What curiosities would it discover that we have yet to find?
So, 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…
Imagine if we could program a computer with all known mathematical truths. What curiosities would it discover that we have yet to find?
Earlier quoted context omitted.
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.
I've re-drafted this several times and it always seems to come out snarky. Please believe me that it's not intended as such - my field is mathematics, not English. So please accept this at face value. I have some expertise in this field. My PhD is in combinatorics, which is closely related, and one of the main results used computer search. More, it's closely related to the Four Colour Theorem. To me, what you say mak…
And, since it's so large, we probably can't do it by hand. So we would need to develop techniques to do it automatically. (Or semi-automatically.)