On the other hand, this is no use for telling you whether main task, solving unsolved mathematics problems, is in NP, since there may be very short mathematical statements that nonetheless have very long proofs. In fact, I believe it has even been proven that the growth rate of maximum proof length exceeds O(n), and as far as I know it may well be exponential.
The shortest proof for a theorem of length n cannot be bounded by any computable function (polynomial, exponential, doubly exponential, whatever). That would directly violate Goedel’s Theorem.
But this does not really affect my proposal. Your power in solving unsolved math problem is directly related to the parameters of your assumed SAT-solver. The better the solver, the longer proofs you will be able to find. But very long proofs are not useful for puny humans anyway. If Riemann has no 10000-page proof, then I am not even interested in finding it.
The shortest proof for a theorem of length n cannot be bounded by any computable function (polynomial, exponential, doubly exponential, whatever). That would directly violate Goedel’s Theorem.
I’m not sure how it would violate Goedel’s theorem, but the statement is correct. Here’s a more direct proof: for any computable function f, you can build a diagonal statement of length n saying “I am not provable in under f(n) symbols in such-and-such formal system”. If the formal system is consistent, then the statement is true (false statements cannot be provable), provable within the system (just enumerate all proofs up to f(n) symbols long), but not provable in f(n) symbols (because it’s true).
If Riemann has no 10000-page proof, then I am not even interested in finding it.
The situation is more subtle. If the RH has no short proofs in ZFC, it could still have short proofs in ZFC+Con(ZFC), and human mathematicians would be interested in that. More generally, not all of math is looking for proofs within existing formal systems. Some of it is picking new formal systems. I’d love to be able to use computers for that, but I don’t know how.
ETA: just noticed that my statement from the first paragraph also works as an example of a statement having a very long proof in ZFC and a very short proof in ZFC+Con(ZFC), as mentioned in the second paragraph :-)
On the other hand, this is no use for telling you whether main task, solving unsolved mathematics problems, is in NP, since there may be very short mathematical statements that nonetheless have very long proofs. In fact, I believe it has even been proven that the growth rate of maximum proof length exceeds O(n), and as far as I know it may well be exponential.
The shortest proof for a theorem of length n cannot be bounded by any computable function (polynomial, exponential, doubly exponential, whatever). That would directly violate Goedel’s Theorem.
But this does not really affect my proposal. Your power in solving unsolved math problem is directly related to the parameters of your assumed SAT-solver. The better the solver, the longer proofs you will be able to find. But very long proofs are not useful for puny humans anyway. If Riemann has no 10000-page proof, then I am not even interested in finding it.
I’m not sure how it would violate Goedel’s theorem, but the statement is correct. Here’s a more direct proof: for any computable function f, you can build a diagonal statement of length n saying “I am not provable in under f(n) symbols in such-and-such formal system”. If the formal system is consistent, then the statement is true (false statements cannot be provable), provable within the system (just enumerate all proofs up to f(n) symbols long), but not provable in f(n) symbols (because it’s true).
The situation is more subtle. If the RH has no short proofs in ZFC, it could still have short proofs in ZFC+Con(ZFC), and human mathematicians would be interested in that. More generally, not all of math is looking for proofs within existing formal systems. Some of it is picking new formal systems. I’d love to be able to use computers for that, but I don’t know how.
ETA: just noticed that my statement from the first paragraph also works as an example of a statement having a very long proof in ZFC and a very short proof in ZFC+Con(ZFC), as mentioned in the second paragraph :-)