= 27d567bc2d48d9f40e9ccc20ea370b15)
Jonathan_Graehl comments on What can you do with an Unfriendly AI? - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (127)
"Finding the shortest proof" given that you already have one is decidable.
If you have a proof of n characters, and your character alphabet has b symbols, then you just have to enumerate and check all the finitely many strings of length 1 (b^1 of them), length 2, (b^2 of them), ..., and of length n-1 (b^(n-1) of them), for proof-ness. If none of those are a proof, then your length n proof is the shortest. Otherwise, the shortest one you found is :)
By "proof" I mean a proof of the statement in question; there are several obvious tweaks to the enumeration process (stopping early, only generating strings that end in QED, generating only syntactically well formed strings, etc), but of course it's still completely impractical if you're going to have to enumerate more than 2^70 or so.
Of course you're both right. In my defense, there is a strong theoretical connection between undecidability and not being in P.
In general, 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. This is independent of how smart the genie is.
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.