[FOM] "Mere" correctness of a proof
Timothy Y. Chow
tchow at math.princeton.edu
Fri Sep 7 12:07:45 EDT 2018
On Fri, 7 Sep 2018, Joe Shipman wrote:
> Tim, your focus on complexity is appropriate, but as far as we know NP
> could equal EXPTIME.
You're right; I should have said NEXPTIME rather than EXPTIME.
> To my way of thinking, any short proof is “explanatory” compared to any
> much longer proof.
> Other notions of “explanatory” seem much more subjective than this one.
I agree that other notions of explanatory are more subjective. On the
other hand, for the purposes of the present discussion, my feeling is that
it is more important to stay close to the intuitive meaning of the word
"explanatory" than to be as objective as possible. Intuitively, I do
agree that an excessively long proof will almost certainly fail to be
explanatory (and that is all I need for my NEXPTIME example to work). On
the other hand, there are plenty of examples of well-known theorems where
the shortest known proof is not the one that most people would find to be
the most explanatory. For example, Zagier's one-sentence proof that every
prime congruent to 1 mod 4 is a sum of two squares is arguably the
shortest known proof of this fact (even after you fill in the elided
intermediate steps), but I have yet to run into someone who finds it to be
the most explanatory proof.
More information about the FOM