[FOM] "Mere" correctness of a proof

[Timothy Y. Chow]

Harvey Friedman wrote:
> A) the first digit of pi is 3.
> B) the sixth digit of pi is 9.
> 
> (recall pi ~ 3.14159)
> 
> This is an interesting arena to test the idea of "explanation of proof".

Another possible arena is computational complexity.  As longtime FOM 
participants know, I am fond of citing the theorem "Checkers is a draw." 
It is hard to imagine an "explanatory proof" of this theorem that does not 
involve brute-force calculation.  Assuming that there is some upper bound 
on how long a proof can be before it ceases to be "explanatory," any 
EXPTIME-complete problem furnishes a family of short theorems which cannot 
all have short proofs.

"Checkers is a draw" could of course be criticized as an unnatural or 
uninteresting mathematical theorem.  But I see no reason why there could 
not exist a short and beautiful theorem for which there does not exist an 
explanatory proof.  (Of course it might be practically impossible to show 
that no explanatory proof exists, so we might be tempted to keep searching 
for one.)  In that event, would Weil have said that God exists because the 
theorem is true, but the Devil exists because we cannot explain why it is 
true?

Tim