there is probably no reasonably short proof, that an arbiter would have time to verify, that a purported proof of the Riemann hypothesis is the shortest.
Agree (“probably”). Would be interesting if there were a proof from complexity theory or elsewhere that it’s expensive to compute in some sense. That we can’t imagine a method is different from a proof that there can’t be one (for proving some general class of “hard to prove/disprove” statements like RH; obviously there’s a constant answer to “shortest proof of a fixed claim”).
If you replace Riemann hypothesis by “any provable mathematical statement” and you allow arbitrary verification procedures instead of just the normal mathematical ones, then the question is probably equivalent to P = coNP, which is equivalent to P = NP.
I assume you’re thinking of this—P=coNP ⇒ polytime decision for propositional tautologies (but not for mixed quanitifier bool. formulas). It’s CoNP-complete to decide tautologies (implicit forall for all the prop. vars) and NP-complete to decide satisfiability (implicit exists for all the prop. vars).
I don’t understand what you mean by “arbitrary verification procedures”—maybe you’re talking about a different result than the one I linked above?
Agree (“probably”). Would be interesting if there were a proof from complexity theory or elsewhere that it’s expensive to compute in some sense. That we can’t imagine a method is different from a proof that there can’t be one (for proving some general class of “hard to prove/disprove” statements like RH; obviously there’s a constant answer to “shortest proof of a fixed claim”).
If you replace Riemann hypothesis by “any provable mathematical statement” and you allow arbitrary verification procedures instead of just the normal mathematical ones, then the question is probably equivalent to P = coNP, which is equivalent to P = NP.
I assume you’re thinking of this—P=coNP ⇒ polytime decision for propositional tautologies (but not for mixed quanitifier bool. formulas). It’s CoNP-complete to decide tautologies (implicit forall for all the prop. vars) and NP-complete to decide satisfiability (implicit exists for all the prop. vars).
I don’t understand what you mean by “arbitrary verification procedures”—maybe you’re talking about a different result than the one I linked above?
Right—those are equivalent.