[cjfd]

I think the type-theoretic outlook on formalized mathematics is actually great, much nicer than set theory anyway. Set theory is a bit like an untyped programming language. You get to ask 'interesting' questions like whether the trivial group is equal to the number 5 which makes sense because both of them are actually a set.

What I am dismayed about is giving yet another area of computing to Microsoft. We all know that Microsoft ensures great care of the long term quality of software, right? Like when you click 'delete' on an email in outlook and have to wait 20 seconds for it to actually disappear.

Why not use coq instead?

[kevinbuzzard]

Lean is free and open source and nothing to do with MS. Check out https://lean-lang.org/ and https://github.com/leanprover/lean4 -- no mention of MS or MSR (where de Moura was where he developed Lean 3 and started on Lean 4).

I have no doubt that a similar project could be done in Coq. The fact that we're using Lean is a random historical coincidence. If we'd used Coq then you could ask "why not Lean".

[msfanboy-aahum]

The main dev of Lean no longer works at MS. So currently there are basically no ties to MS. Lean is developed by the Lean FRO, which aims at being selfsustainable in ~4 yrs from now.

[practal]

Type theory vs. set theory is not the only choice. It is possible to combine their strengths in a new foundation: A single mathematical universe, just as in set theory, and higher-order features and abstraction, just as in type theory. Note that the listed strengths of each are the weaknesses of the other.