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.
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.