Topic: why lean for math?
Kevin Tran (Sep 08 2020 at 13:13):
what sets lean apart from other theorem provers like coq and isabelle for math?
Adam Topaz (Sep 08 2020 at 13:15):
In my opinion... This zulip server.
Kevin Buzzard (Sep 08 2020 at 14:48):
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 (Sep 08 2020 at 14:51):
sounds like the right place for me then
Patrick Massot (Sep 08 2020 at 15:07):
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).
Last updated: May 06 2021 at 19:30 UTC