where does lean really stand?

Stream: general

[Arthur Paulino]

In my learning trajectory about formal proofs, I started out with Coq and then jumped into Lean. This is also my first true experience with a functional programming language. I've used Scala, but mostly as a means to use the Spark API. In summary, this is being a complete breakthrough in my understanding about CS (and mathematics).

However, since this is all very new to me, I would like to understand more about what distinguishes Lean from other languages and proof assisting tools. Where does Lean shine and which are its drawbacks? Does anyone know a good material on this subject?

[Julian Berman]

I'll throw in a stack overflow post by @Andrej Bauer that I read yesterday which was quite nice -- https://mathoverflow.net/a/376973
Undoubtedly others will share more general resources but I found that a nice distilled bit to read at my level.

[Kevin Buzzard]

One thing about lean is that tactics are written in Lean. This means that Rob and Johan can write a paper about Witt vectors together which introduces new theorems and constructions and also new bespoke tactics which can be used with these constructions a coherent manner, just with lean files

[Kevin Buzzard]

Another thing is that lean has a gigantic classical mathematics library for possibly sociological reasons and this library will soon dwarf other libraries of this form

[Anne Baanen]

If I understand your question as 'What qualities does Lean have as a piece of theorem proving software?' (not as 'Why might Lean be a good choice for formalizing "modern" maths?' for which the answer is much more sociological I expect):

Foundationally, quotient types and proof irrelevance. In the user interface, a nicer tactic system (which I still find extremely hard to find my way around in, FWIW...). I also happen to like typeclasses, and Lean features a good implementation of them which makes setting up a decent hierarchy quite a bit more manageable than the quite careful discipline of canonical structures.

[Anne Baanen]

As far as I can tell, the features that Coq provides for typeclasses are quite similar in their design to Lean's. But in the Coq community there seems to be a common belief that classes are inefficient, which is true up to some extent, since synthesizing an instance requires a whole Prolog-like backtracking search. Also one of the first big class-based algebraic hierarchies for Coq was basically totally unbundled, which can really blow up the sizes of terms, and furthermore Coq seems to do a bit worse when terms become really big. Canonical structures are hard to get right by hand, so the mathcomp community designed a metaprogram Hierarchy Builder to do it for them. Especially since the metaprogram is written in a dialect of Prolog, this feels like Greenspun's 10th rule but for typeclasses instead of Lisp :)

[Anne Baanen]

Can you tell I have been thinking a lot about typeclasses recently? :grinning:

[Arthur Paulino]

One thing I don't understand is why so much nitpicking about being able to say $2 \in 3$ while you can design the natural numbers using sets such that $2 \in 3$ would no longer hold. For instance, $\emptyset$ would define zero, $\{\{\emptyset\}\}$ would define 1, $\{\{\{\{\emptyset\}\}\}\}$ would define 2, so on and so forth. Would this cause a lot of trouble?

Anyway, this is a bit offtrack...

[Anne Baanen]

It doesn't make me feel a lot better to know that the answer to "Is $2 \in 3$?" is "no" instead of "yes". My real objection is that the question does not make sense, or at least is irrelevant if we're talking about natural numbers. If you get my point.

[Eric Rodriguez]

I mean, $n \in n+y+1$ is almost a feature to encode <; things like $\pi \in \aleph_0$, or whatever are far more nonsensical to me

[Anne Baanen]

As for ordinals, sure, I'll accept $2 ∈ 3$ as sensical and true.

[Arthur Paulino]

I get your point. You're saying that $2 \in 3$ should neither evaluated as "true" nor "false". It should just "break", in some sense

[Anne Baanen]

Indeed, I'd argue "type error" is a more natural answer to the question than yes or no.

[Arthur Paulino]

What made me choose learning Lean over Coq was... the language syntax. Somehow, Lean felt a lot more like home for someone with a CS/programming background like me

[Anne Baanen]

Coming from Haskell, Agda still holds the number one position in my eyes. Though Lean is in a solid second place. :grinning:

[Kevin Buzzard]

In a parallel universe we're trying to do mathlib in some flavour of agda. Classical mathematics libraries just aren't their thing though. Might only be sociological. I still don't know if we just got lucky with Lean or whether manifolds and perfectoid spaces would have been just as easy to define in Agda. The theorists all tell me that in theory it's possible to do but nobody does it in practice. So now you have to decide whether it's worth the years of experimenting. I think it is, but I'm not going to do it myself, I've already spent 2 years learning a system and I want to keep going forwards

[Joe Hendrix]

For my part, I initially started with Lean in the Lean 2 days, and at the time was excited about a proof assistant based on dependent types that could also be used as a library for integration with automated tools. I had created a library like this in Haskell called SAWCore, but thought Lean was much better thought out and more mature.
Now with Lean 4, I'm excited about Lean 4 because of the syntax, efficient compilation with a small runtime, strong potential for building automation, and interest by the math community for building libraries and automation. I know there are some efforts to build efficient compilers for other proof assistants, but I think the combination of features keeps me most excited by Lean.