Occam’s razor still applies. If we’re looking for the most elegant possible proof of a theorem (whatever that means), any sufficiently short proof is much more likely to be it than any sufficiently long proof. If you want to take a completely wild guess about what statement an unknown theorem proves, you’re better off guessing short statements than long ones.
If we’re looking for the most elegant possible proof of a theorem (whatever that means), any sufficiently short proof is much more likely to be it than any sufficiently long proof.
Could you try to make that statement more precise? Because I don’t believe it.
If you take the shortest possible proofs to all provable theorems of length less than N, both the maximum and the average length of those proofs will be extremely (uncomputably) fast-growing functions of N. To see that, imagine Gödel-like self-referential theorems that say “I’m not provable in less than 3^^^^3 steps” or somesuch. They’re all true (because otherwise the axiom system would prove a false statement), short and easy to formulate, trivially seen to be provable by finite enumeration, but not elegantly provable because they’re true.
Another way to reach the same conclusion: if “expected length of shortest proof” were bounded from above by some computable f(N) where N is theorem length in bits, we could write a simple algorithm that determines whether a theorem is provable: check all possible proofs up to length f(N)*2^N. if the search succeeds, say “yes”. If the search fails, the shortest proof (if it exists) must be longer than f(N)*2^N, which is impossible because that would make the average greater than f(N). Therefore no shortest proof exists, therefore no proof exists at all, so say “no”. But we know that provability cannot be decidable by an algorithm, so f(N) must grow uncomputably fast.
If we’re looking for the most elegant possible proof of a theorem (whatever that means), any sufficiently short proof is much more likely to be it than any sufficiently long proof.
Could you give a precise meaning to that statement? I can’t think of any possible meaning except “if a proof exists, it has finite length”, which is trivial. Are short proofs really more likely? Why?
Occam’s razor still applies. If we’re looking for the most elegant possible proof of a theorem (whatever that means), any sufficiently short proof is much more likely to be it than any sufficiently long proof. If you want to take a completely wild guess about what statement an unknown theorem proves, you’re better off guessing short statements than long ones.
Could you try to make that statement more precise? Because I don’t believe it.
If you take the shortest possible proofs to all provable theorems of length less than N, both the maximum and the average length of those proofs will be extremely (uncomputably) fast-growing functions of N. To see that, imagine Gödel-like self-referential theorems that say “I’m not provable in less than 3^^^^3 steps” or somesuch. They’re all true (because otherwise the axiom system would prove a false statement), short and easy to formulate, trivially seen to be provable by finite enumeration, but not elegantly provable because they’re true.
Another way to reach the same conclusion: if “expected length of shortest proof” were bounded from above by some computable f(N) where N is theorem length in bits, we could write a simple algorithm that determines whether a theorem is provable: check all possible proofs up to length f(N)*2^N. if the search succeeds, say “yes”. If the search fails, the shortest proof (if it exists) must be longer than f(N)*2^N, which is impossible because that would make the average greater than f(N). Therefore no shortest proof exists, therefore no proof exists at all, so say “no”. But we know that provability cannot be decidable by an algorithm, so f(N) must grow uncomputably fast.
Could you give a precise meaning to that statement? I can’t think of any possible meaning except “if a proof exists, it has finite length”, which is trivial. Are short proofs really more likely? Why?
More emphasis on the most elegant possible.
Sorry for deleting my comment, I got frustrated and rewrote it. See my other reply to grandparent.
I don’t believe it either, by the way.