[FOM] EFQ and Faithful Formalization

[Timothy Y. Chow]

Alan Weir wrote:

> To take an extreme example: if there actually is a formal PA proof of 
> Fermat's Last Theorem there is a clear sense it will not be a faithful 
> representation of Wiles' proof, since the latter brings in content from 
> branches of mathematics other than arithmetic.

This remark surprises me.  Can we infer that there is a clear sense in 
which a formal ZFC proof of any theorem of a paper with a Mathematics 
Subject Classification number other than 03Exx (set theory) will not be 
faithful to the original proof, because the latter brings in content from 
branches of mathematics other than set theory?

This seems fundamentally wrong since any formalization of any theorem 
surely starts with a very small set of basic concepts, but then by the 
above criterion, it will be hopeless to "faithfully represent" any theorem 
of algebraic topology or microlocal analysis or p-adic representation 
theory since such a theorem will by its very nature contain content from 
branches of mathematics that go beyond the initial set of basic concepts.

Tim