> except serve as a basis for practical formalization of proofs I do formalized mathematics as a hobby and I can not see any basis for that opinion. Freek Wie

> except serve as a basis for practical formalization of proofs I do formalized mathematics as a hobby and I can not see any basis for that opinion. Freek Wiedijk wrote an interesting paper [0] where he compared the complexity of various foundations as encoded in Automath. Mizar, which is based on Tarski–Grothendieck set theory (an extension of ZFC) is a proof assistant whose library was the largest for a couple of decades, only recently surpassed by Lean's Mathlib (perhaps). Metamath is mentioned below in comments and of course my favorite Isabelle/ZF are also based on ZFC. [0] [Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics] (https://www.sciencedirect.com/science/article/pii/S1570868305000765 https://www.sciencedirect.com/science/article/pii/S157086830...)