[FOM] "Mere" correctness of a proof

[Timothy Y. Chow]

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.

https://people.mpim-bonn.mpg.de/zagier/files/doi/10.2307/2323918/fulltext.pdf

Tim