EDIT: It is a fair point that it is difficult to say what is easier to implement (the below expands on this). By type theory being natural I was mostly thinking of the fact that it is basically a functional programming language with a very strict compiler.
Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible.
Also, this means if you are counting lines you need to include the formalisation of the logic and the axioms of ZFC inside metamath. The kernel of Coq is similarly a quite short program.
Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones (For instance the first formalised proof of the four colour theorem and Gödel’s theorems were in Coq).
> Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible.
That's true. There's a Metamath database that encodes Higher-Order Logic (HOL) aka simple type theory: http://us.metamath.org/holuni/mmhol.html It's very bare-bones, but it shows it's possible.
> Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones...
I suspect we have to ask "popular for whom?" I'd agree that type theory is at least as popular as set theory among computer tools that formalize math. But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. Type theory probably seems "natural" to people who are used to programming languages and compilers, and thus already have a daily familiarity with types (in the computer science sense).
"It's complicated" seems like an accurate summary of affairs :-).
> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics.
Most mathematicians spend very little time thinking about the foundations of mathematics though, so I'd take that with a grain of salt. ;)
Seriously though, I think the statement that "all of modern mathematics can be formalized in ZFC" is probably wrong. There have been attempts to do just that (e.g., Bourbaki), but they invariably failed and ended up with extensions of ZFC (e.g., for category theory) or just silently started using higher-order logic.
Type theory seems to be a lot more practical. Both because it is explicitly designed to be an open system (a closed system must fail eventually due to Gödel arguments) and because similar formalization efforts go a lot more smoothly. For example, compare the treatment of category theory in the HoTT book with any introductory text using set theory.
> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics.
That's true, but it's just as true that those same mathematicians only care about foundations as a proof of concept, not a practical device that you might someday want to do actual math in. ZFC is plenty good enough for the former, but you need type theories - or at least structural-set theories - to enable the latter (with the sorts of sanity checks that we've come to expect in any practical formal endeavor)!
Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible.
Also, this means if you are counting lines you need to include the formalisation of the logic and the axioms of ZFC inside metamath. The kernel of Coq is similarly a quite short program.
Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones (For instance the first formalised proof of the four colour theorem and Gödel’s theorems were in Coq).