FOM: Mizar proofs

[Harvey Friedman]

I wish to sincerely thank Andrzej Trybulec of the Mizar project for his
thoughtful posting of 3:19PM 4/12/99.

>   The time needed for formalization is extremely difficult to estimate.
>   Proving Hahn-Banach theorem took 3 days, if I recall. On the other
>   hand the proof of the Jordan curve theorem we started in 1991 and
>   as yet it is proved only for polygonal curves (actually a special case:
>   for polygons with edges parallel to axes).

I meant to ask a different question. What I meant was: what is the estimate
on the length of formal proofs? [The time question is also interesting;
thank you for answering it.]

I am under the impression that the Mizar project not only gets the machine
to accept derivations, but also creates a proof in a reasonable system, the
details of which can be specified in advance.

E.g., how long is an appropriately formal proof of Fermat's Last Theorem?