The idea of Lean working for all of math is absurd though, . You are very quotable, but come on, that is sensationalist, the assumption of UIP alone rules out many kinds of mathematics.
Conversation
The vast, vast majority of mathematicians make vague gestures towards ZFC and then forget about foundations. Formalising maths as it is now is fine with UIP. Formalising it as it could be is a whole different story.
1
2
But "vast majority" and "all" are very different things, and mathematicians know this well
1
We already know we can't formalise "all" of maths, cf. Gödel. Any project that claims to desire that really means "the maths that we need to do lots of useful maths".
1
2
The consequence of that though is that we need different kinds of foundations to cover all of math, and that is important---different tools for different purposes. I just don't like big bold statements that claim more than they mean. But I'm talking to Kevin about this later
1
1
In general I agree. Even from a proof engineering perspective, Lean is nice but a lot of what it does Isabelle also does and has done for a long time. (Incidentally, Isabelle technically supports many different foundations, but I dunno if anyone's made a Isabelle/CubicalTT).
2
4
That's a point that I always found confusing. Is it really so easy to implement dependent types in Isabelle? Its meta-theory is simply typed. Surely, someone has tried.
1
2
Paulson did it. There is a seldom used Isabelle/ITT
1
Oh, it’s not ITT, I misremembered.
1
1
Hah was about to say 'woops, that's CTT, not ITT' 😅
Yeah I've found it cool to look at some of the other ones linked under "Theory libraries for Isabelle2020", but I never really know what I'm looking at, haha: mirror.cse.unsw.edu.au/pub/isabelle/d
Isn't the rough story that he implemented extensional type theory, but then everyone in Cambridge said that he'd implemented the wrong one, so he gave up?