[FOM] Translating ``every'' theorem of mathematics?

[Timothy Y. Chow]

On Sun, 30 Dec 2007, Dr. M. Insall wrote:
> Claim 0:  There exists a set S of scientists such that if T is a theorem 
> of ordinary mathematics, and if t is any time, and if M is any 
> mathematician, and mathematician M proves theorem T at time t, then some 
> scientist s in S will at some time t' translate theorem T into a formal 
> language.

It's true that the claim I made may have been exaggerated, and I'm not so 
much interested in defending this claim as I am in the Formalization 
Thesis (or more precisely, in the project of giving the "Formalization 
Thesis" a name).  So if you wish to doubt it, I'm not going to argue very 
fervently with you.  I will, however, point out that underlying your 
arguments seems to be a tacit assumption that artificial intelligence will 
never advance to the point where machines can read math papers *in their 
present form* and convert them into formal proofs.  While I don't believe 
that such a point will be reached in any of our lifetimes, I think it's a 
possibility.  If your set S of scientists includes robots then Claim 0 
seems less implausible than if S is restricted to human beings.

Tim