A Survey of Languages for Formalizing Mathematics

Stream: general

[Jason Rute]

This A Survey of Languages for Formalizing Mathematics mentions Lean just a little bit.

[Scott Morrison]

It seems lack of subtyping rules us out. :-)

[Kevin Buzzard]

I'm quite happy to let computer scientists theorise about formalising mathematics, whilst the community here is actually doing it, and at an extraordinary rate

[Kevin Buzzard]

And I think might have an idea of what mathematics is which is closer to what mathematicians think mathematics is