19 Mar
2012
19 Mar
'12
1:05 p.m.
On Monday 19 March 2012 01:58:59 Henry Baker wrote:
Proof _checking_ is a purely mechanical, almost linear complexity (in the length of the proof) problem (depending upon the representation). _Finding_ a proof is the hard part, and can be multiply- (?) exponential in the length of the proof.
Clearly not multiply-exponential, given that proof checking is of approximately linear complexity. All you have to do is enumerate all possible proofs (there are singly-exponentially many) and check them one by one. -- g