why lean for math?

Stream: maths

[Kevin Tran]

what sets lean apart from other theorem provers like coq and isabelle for math?

[Adam Topaz]

In my opinion... This zulip server.

[Kevin Buzzard]

The community here contains mathematicians who are working in areas like number theory, geometry, topology, analysis etc, rather than people interested in foundations. As a result a lot of number theory, geometry, topology, analysis is getting done here, and the library has taken on an extremely non-constructive tone. This is one difference from Coq (which is much more constructive in general). A big difference with Isabelle/HOL is that we use a stronger logic.

[Kevin Tran]

sounds like the right place for me then

[Patrick Massot]

Note that "stronger logic" is not a magic incantation. It means that many things are expressed more naturally, but the counter part is that automation is less powerful. One day we'll have strong logic and strong automation in the same software (Lean 4 hopefully).