Last week, I asked the "automated proof-checking machine." Many answered that automated proof-checking machine already exists in first-order theory.
However I have still question. For the operation of 'automated proof-checking machine', the input (mathematical proof) must be transformed into 'well formed formula'.
I found an article which insists that well formed formula include all theorem.
http://en.wikipedia.org/wiki/Formal_language
Is it possible that all proof (maybe in ZFC) can be transform as formal language (well-formed formula) ?
Yes, the set of formal proofs is a formal language in itself. It is not the same as the formal language of formulas, though. For example, we might define a proof to be a certain kind of finite sequence of formulas, or we might define a proof to be a certain kind of labeled finite tree.