hol mathlib

Stream: general

[Huỳnh Trần Khanh]

can mathlib be written in Isabelle/HOL or HOL Light? this is a question, not a suggestion

[Huỳnh Trần Khanh]

or a better wording would be: is the logical foundation of HOL systems strong enough for mathlib

[Mario Carneiro]

Others will say no, dependent types are required for certain constructions. In truth you can always add the axioms of ZFC or what have you and have all the dependencies you need, so it's possible in principle. (You don't even need anything past FOL for ZFC.) But automation support would have to be written from the ground up. Again, doable in principle, but it would make enough of a break from the existing libraries that it may as well be "lean ported to HOL light / isabelle" rather than coexisting with the libraries that are already there.

[Mario Carneiro]

That's assuming a very rigid definition of what mathlib is in terms of theorem statements. If you are okay with vaguely analogous theorems then it's already happening for the most part, although @Sebastien Gouezel is an isabelle refugee who can probably tell you more about where the lack of dependent types cause practical problems for formalization.