Overwhelming prior makes my claim more likely to be correct than the majority of claims made by myself or others. ;)
Very Bayesian of you! This is potentially confusing, though, in that you made a mathematical claim. Frequently mathematical claims mean that you have a proof of something, not that it’s very likely. This issue comes up with computerized proofs in mathematics, like the four-color theorem. It’s very likely to be true, and is usually considered proven, but we don’t actually have a formal proof, only a computer-based one.
Note that your logic would apply equally well to Mersenne primes of N digits, for sufficiently large N. This makes sense in a Bayesian framework, but in a mathematical framework, you could take these statements and “prove” that there were a finite number of Mersenne primes. Mathematical proofs can combine in this way, though Bayesian statements of near-certainty can’t. For instance, for any individual lottery ticket, it won’t win the lottery, but I can’t say that no ticket will win.
Actually, Georges Gonthier did give a formal (computer-verified) proof of the four-color theorem. Also, I believe that before that, every 5 years, someone would give a simpler version of the original proof and discover that the previous version was incomplete.
Wow, thanks! I didn’t realize that. It looks like Gonthier’s proof was verified with Coq, so it’s still not clear that it should count as a proof. I’m still waiting for the Book proof.
Very Bayesian of you! This is potentially confusing, though, in that you made a mathematical claim. Frequently mathematical claims mean that you have a proof of something, not that it’s very likely. This issue comes up with computerized proofs in mathematics, like the four-color theorem. It’s very likely to be true, and is usually considered proven, but we don’t actually have a formal proof, only a computer-based one.
Note that your logic would apply equally well to Mersenne primes of N digits, for sufficiently large N. This makes sense in a Bayesian framework, but in a mathematical framework, you could take these statements and “prove” that there were a finite number of Mersenne primes. Mathematical proofs can combine in this way, though Bayesian statements of near-certainty can’t. For instance, for any individual lottery ticket, it won’t win the lottery, but I can’t say that no ticket will win.
Actually, Georges Gonthier did give a formal (computer-verified) proof of the four-color theorem. Also, I believe that before that, every 5 years, someone would give a simpler version of the original proof and discover that the previous version was incomplete.
Do you have a reference for the ‘discover that the previous version was incomplete’ part?
Wow, thanks! I didn’t realize that. It looks like Gonthier’s proof was verified with Coq, so it’s still not clear that it should count as a proof. I’m still waiting for the Book proof.