Lean is well engineered, is also marketed as a programming language, and expressive enough to do proper math in it. Type theory is more elegant to implement tha

Lean is well engineered, is also marketed as a programming language, and expressive enough to do proper math in it. Type theory is more elegant to implement than set theory based on first-order logic. That's about it. Nevertheless, first-order logic is not the last word when it comes to formalising set theory, I think Abstraction Logic (AL)[1] is. When you start formalising set-like and type-like things in AL, the border between sets and types disappears. That border is just an artefact of history, useful for foundational studies, but will lose its importance for anything practical. [1]: https://obua.com/publications/philosophy-of-abstraction-logic/2/ https://obua.com/publications/philosophy-of-abstraction-logi...