features of Lean/Lean4

Stream: new members

[Robert Watson]

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]

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

[Patrick Massot]

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

[Robert Watson]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Robert Watson]

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

[Patrick Massot]

Normal maths for Lean 3.

[Patrick Massot]

Programming in a self-verified language for Lean 4.

[Patrick Massot]

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

[Robert Watson]

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]

You got there before me...

[Robert Watson]

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

[Patrick Massot]

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]

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]

Interesting. Really interesting. What about constructive mathematics?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Robert Watson]

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

[Robert Watson]

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

[Patrick Massot]

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]

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]

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]

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

[Robert Watson]

Thanks again.

[Patrick Massot]

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

[Patrick Massot]

if you care about that sort of things

[Patrick Massot]

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