Zulip Chat Archive

I was wondering (currently working through Lean tutorial exercises) - what are the advantages/disadvantages of Lean compared to other proof assistants? What can't it do/what isn't it good for/what are its limits? I am really enjoying exploring it so far, but I'm wondering what the roof of the sky is, you know?

Patrick Massot (Aug 20 2020 at 15:45):

There are a couple of pointers at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/CICM.202020/near/206476084. But discussing this is not so fertile. You can simply try a couple of proof assistants. If you don't know where to start in order to learn Coq then you probably want to use Lean...

Wrenna Robson (Aug 20 2020 at 15:48):

That's fair enough!

Wrenna Robson (Aug 20 2020 at 15:52):

I suppose what I was trying to get my head round was why a project that already exists and uses Coq might use Coq in specific, say, but I suppose to a degree the answer is "time exists and we live now and not then", which isn't particularly fertile.

Patrick Massot (Aug 20 2020 at 15:58):

There is a lot of inertia here. Learning how to use a proof assistant is extremely time-consuming, and changing is difficult. Building a good library is also extremely time-consuming and discourages switches. There are also huge cultural differences that totally prevents many movements between communities. The Coq community has a huge bias towards constructive mathematics while most people here do regular mathematics. This is not a difference between software, but between people and libraries.

Wrenna Robson (Aug 20 2020 at 16:33):

That makes sense. I'm coming at it from a cryptography perspective and wondering if I might be able to get any use from it. Well: let me be more exact. I'm wonder if I could extract some useful research by writing some provable security stuff in Lean. Somebody has to be the first...