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.
Many experts suspect that there is no polynomial-time solution to the so-called NP-complete problems, though no-one has yet been able to rigorously prove this and there remains the possibility that a polynomial-time algorithm will one day emerge. However unlikely this is, today I would like to invite LW to play a game I played with with some colleagues called what-would-you-do-with-a-polynomial-time-solution-to-3SAT? 3SAT is, of course, one of the most famous of the NP-complete problems and a solution to 3SAT would also constitute a solution to *all* the problems in NP. This includes lots of fun planning problems (e.g. travelling salesman) as well as the problem of performing exact inference in (general) Bayesian networks. What's the most fun you could have?