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 <i>can</i> check myself. In such a chain, the truth of the final result is not, to me, in dispute.<p>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.<p>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?
"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.<p>A minor thing, but comparisons like this always drive me nuts. Just say "13GB proof too big for humans to check." Then there's no confusion.</sillyrant>
"The set-theoretical axioms that sustain modern mathematics are self-evident in differing degrees. One of them – indeed, the most important of them, namely Cantor's axiom, the so-called axiom of infinity – has scarcely any claim to self-evidence at all". John P. Mayberry
From the linked Wikipedia article:<p>> All experiments were conducted on PCs equipped with an Intel Core i5-2500K CPU running at 3.30GHz and 16GB of RAM.<p>Why are these experiments not being conducted on a more powerful computer or a cluster?