Notices by NoCanDo (escape_velocity@functional.cafe)

@julesh I sincerely doubt that. For one, lean might have a ZFC model, but it is still a CoC system + UIP + 3 axioms. Secondly, mathematicians don't give two hoots about ZFC or any foundations. I learnt this only 2-3 years ago. Talking about foundations is pretty much the same as flogging a dead horse that can never be revived by any magic. With mathlib and lean, this conversation has become even more difficult. Thirdly, in lean, especially mathlib, definitions are separated from useful theorems by a layer of API lemma. So if definitions have to change while maintaining the same properties, only the API lemmas need to be reproved. Everything else stays the same, unless something fundamentally changes in the type system.

Finally IMHO, among other socio-cultural things, what made lean so popular today is UX. When this perfect proof system is built, I hope the developers invest heavily in UX. Someone might build the greatest proof system on the planet, but if they insist on pushing UX of a bygone era, then the system will never compete against another with better UX. Tooling matters. Easy package management matters*. In general, the "boring" stuff matters. Much more than interesting foundational conundrums or features. If a language does not have decent editor support (that means vscode today), then I am not touching it with a barge pole. I still poke around in other ITPs and even enjoy them a bit, but none can yet match lean's editor support. That's the biggest lesson I learnt from the lean community.

* lean's highly annoying and deficient package management still feels leaps and bounds ahead of what I have seen in other ITPs