Zulip Chat Archive

Stream: new members

Topic: features of Lean/Lean4


Robert Watson (May 08 2021 at 14:47):

Hi all, I'd like to know: why use Lean(4?)? My impression is that it is a replacement for Coq. But what are the advantages of Lean over Coq in that case? How does it then also differ from Agda which is also an alternative to Coq?

Patrick Massot (May 08 2021 at 15:07):

It very much depends on what you want to do. Those software and their libraries have different strength.

Patrick Massot (May 08 2021 at 15:07):

Are you interested in traditional mathematics, logic, software verification or type theory?

Robert Watson (May 08 2021 at 15:31):

Yes. All of the above. Plus constructive mathematics. Plus programming in a self-verified language.

Johan Commelin (May 08 2021 at 15:34):

If you are interested in all of those, you should really try all of the systems.

Johan Commelin (May 08 2021 at 15:35):

Because (currently) none of the systems is good for all of those interests at the same time.

Robert Watson (May 08 2021 at 16:03):

Which hat should I wear when I start to use Lean?

Patrick Massot (May 08 2021 at 16:04):

Normal maths for Lean 3.

Patrick Massot (May 08 2021 at 16:04):

Programming in a self-verified language for Lean 4.

Patrick Massot (May 08 2021 at 16:05):

Note that Lean 4 will also be great for maths in the future, but it's not yet read for that.

Robert Watson (May 08 2021 at 16:06):

That's kind of why I'm asking the question, isn't it. Presumably Lean 4 is expected to catch up with Lean 3 for libraries at some point?

Robert Watson (May 08 2021 at 16:06):

You got there before me...

Robert Watson (May 08 2021 at 16:07):

I can't find anything on the internet for input/output in Lean 4...IO monads?

Patrick Massot (May 08 2021 at 16:12):

Documentation of Lean 4 is still very much WIP. You can already have a look at https://github.com/leanprover/lean4/blob/master/src/Init/System/IO.lean

Kevin Buzzard (May 08 2021 at 16:19):

Yes, lean 3's main library is its maths library mathlib and we fully expect the hard job of porting it to lean 4 to occur at some point -- people are actively thinking about it

Robert Watson (May 08 2021 at 16:27):

Interesting. Really interesting. What about constructive mathematics?

Kevin Buzzard (May 08 2021 at 16:27):

mathlib is developed as a classical library, most mathematicians here are not constructivists.

Kevin Buzzard (May 08 2021 at 16:29):

My personal rationale for this is that the constructivists have had a pretty tight hold on computer theorem provers for decades, and the provers didn't catch on in maths departments (where constructivists are vanishingly rare) so it's time to have a go with a classical maths library to see if this generates any more excitement amongst mathematicians.

Patrick Massot (May 08 2021 at 16:36):

Honestly if you are interested in constructive mathematics you'll feel much better in the Coq community. You're still welcome here, but you'll be sad.

Robert Watson (May 08 2021 at 16:36):

Does that preference have any engineering consequences for the underlying implementation of the type system/kernel and elaboration?

Kevin Buzzard (May 08 2021 at 16:37):

It just makes most of it (the library) noncomputable, but as a classical mathematician I don't care about this because all I want to do is prove more theorems (I realise I'm not answering your question, I think the answer is "no")

Robert Watson (May 08 2021 at 16:42):

This is fascinating. I believe in using both styles btw. But I want tight control over which I am using and when.

Robert Watson (May 08 2021 at 16:43):

Is there an issue like the way NuPRL has an undecidable type system?

Robert Watson (May 08 2021 at 16:44):

(I've already decided Lean 4 > Lean 3 btw.)

Patrick Massot (May 08 2021 at 16:46):

This is has almost nothing to do with the kernel. It's mostly the library and the user community (those are mostly equivalent concepts).

Robert Watson (May 08 2021 at 16:47):

Yes. In other words, this makes no real difference in the long term. Thanks guys...much as I could go on for hours I'll give you a break. Thanks indeed and see you around.

Patrick Massot (May 08 2021 at 16:48):

I wrote almost nothing because the tiny variations between Coq's type theory and Lean type theory do have some consequences. Definitional equality is undecidable.

Patrick Massot (May 08 2021 at 16:49):

see Section 3 from https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf

Robert Watson (May 08 2021 at 16:49):

Thanks again.

Patrick Massot (May 08 2021 at 16:51):

see also https://arxiv.org/abs/1911.08174

Patrick Massot (May 08 2021 at 16:51):

if you care about that sort of things

Patrick Massot (May 08 2021 at 16:51):

None of this has any impact on mathematics formalization of course.


Last updated: Dec 20 2023 at 11:08 UTC