[FOM] "Mere" correctness of a proof
Timothy Y. Chow
tchow at math.princeton.edu
Thu Sep 6 14:19:23 EDT 2018
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
More information about the FOM