[FOM] formal proofs

[Timothy Y. Chow]

Harvey Friedman wrote:

> So again, I'll repeat my request in more focused form. We need the
> simplest toy example of where there starts to be a problem in normal
> formalization.

I don't understand your point here.  It sounds to me like you're insisting 
that someone state precisely the minimum number of grains of sand in a 
heap.  Why is that necessary?

It seems to me that the "Blakers-Massey challenge," as spelled out in more 
detail by David Roberts, is a fine challenge.  If it is met, then the 
traditionalists "win."  If not, then presumably the difficulties 
encountered along the way will reveal where the critical problem or 
problems lie.  I don't see why the sticking points need to be spelled out 
in advance.

Tim