[FOM] Translating ``every'' theorem of mathematics?
Timothy Y. Chow
tchow at alum.mit.edu
Sun Dec 30 16:49:07 EST 2007
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
More information about the FOM
mailing list