[FOM] "Mere" correctness of a proof

[Joe Shipman]

Tim, your focus on complexity is appropriate, but as far as we know NP could equal EXPTIME.

To my way of thinking, any short proof is “explanatory” compared to any much longer proof. Harvey has shown plenty of results where a class of theorems with only very long proofs in weaker systems have short proofs in stronger systems, and this is a basic principle reverse mathematics has taught us: the most “explanatory” possible proof is one which shows that the theorem (or the universally quantified version of a sequence of theorems) is equivalent (over a weaker system) to a statement generally recognizable as “axiomatic”.

Other notions of “explanatory” seem much more subjective than this one.

However, we also have a gold standard for “non-explanatory” proofs, namely “zero-knowledge” proofs from complexity theory. These are usually interactive, but under strong cryptographic assumptions, there exist zero-knowledge proofs which require an amount of effort to check that is polynomial in the length of the statement being proved. (Whether the check shows the theorem to be true or whether it merely shows the theorem to be false with exponentially tiny probability depends on whether your strong cryptographic assumption is of the form “h is an ideal hash function” or “Almost all hash functions in the class H are cryptographically ideal”, respectively; the former seems much more likely than the latter to be unprovable in ZF.)

— JS

Sent from my iPhone

> On Sep 6, 2018, at 2:19 PM, Timothy Y. Chow <tchow at math.princeton.edu> wrote:
> 
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom