FYI (Avigad on Varieties of Math Understanding)

[Timothy Y. Chow]

Vaughan Pratt wrote:
> My first thought was to post the following question to Quora:
> https://www.quora.com/unanswered/Are-there-any-theorems-that-are-accepted-by-most-mathematicians-as-true-as-opposed-to-merely-a-conjecture-yet-for-which-no-rigorous-proof-has-been-found-as-yet
>
> Rather than comment here I'll just say that the second part of my answer to
> my own question explains how Avigad's article prompted my question.

I'd suggest that what mathematicians mean by a "correct" proof is an 
argument that could, if desired, be fleshed out to meet any desired 
standard of rigor.  The operative word here is "could."  For the proof to 
be declared correct, the fleshing out doesn't have to be actually carried 
out; people just have to be convinced that it *could* be fleshed out.

On Quora, you asked, "Is there any notion of rigor met by all published 
“correct” proofs of theorems that is not ultimately computational in 
nature?"  It is tacitly understood that mathematicians always have the 
right to request further fleshing out.  Typically, people exercise this 
right only when they can't see how to flesh things out themselves.  But if 
you decide that only a formal, computational proof will satisfy you, and 
you always exercise your right to request more details in the absence of 
that, then you can (seemingly) demonstrate that "all correct proofs are 
computational."  But others who choose not to exercise that right might 
disagree that all correct proofs are computational, because they stop 
requesting further fleshing out long before that point.

Here's an analogous question.  Is there any form of payment that is not 
ultimately barter?  Sure, you might say; I can pay cash.  But people 
accept cash only because they have confidence that the cash can later be 
exchanged for goods, so you could argue that "ultimately" when you pay 
cash, you're bartering.  On the other hand, many people are happy not only 
with cash, but with credit cards.  With a credit card, you're not even 
paying cash; you're convincing someone that you can give them cash later. 
Some countries are moving toward being "cashless"; transactions in a 
cashless society certainly don't *look* like barter.  Nevertheless, you 
can point out that if something causes a crisis of confidence, then people 
will tend to revert to barter, so that's the ultimate foundation of 
economic transactions.

Tim