[FOM] Formalization Thesis

[Freek Wiedijk]

Andrej:

>People who actually work on formalization know that
>having powerful type-theoretic infrastructure is absolutely
>necessary to keep things organized (imagine having 3000
>lemmas...). So they use type theory instead.

Nonsense.  Of the systems that are the most interesting for
formalization of mathematics (the various HOLs, Isabelle,
Coq, Mizar, maybe PVS) only Coq is based on type theory.
The rest all are as classical as possible.

Or do you call a system based on "type theory" whenever it
is has a notion of type?  That would be strange: Mizar has a
very interesting kind of types, but it is _very much_ based
on set theory.  _(And_ it has the biggest library of them
all, with an order of magnitude more lemmas than you quote.)

Freek