soft question: what makes lean lean

Stream: general

[Nick Dean]

Soft question if anyone has a take. How does lean4 compare to Coq/Agda/Isabelle/... (either a particular example or as a group if you take there to be larger groupings) in terms of its approach, motivations, aspirations, ... things like that? For context by way of example, I note that some frameworks for formalized mathematics seem particularly interested in HoTT and univalent foundations, others not so much. Put another way, is there anything lean 4 defines itself by from a super high level perspective? Thanks

[Kevin Buzzard]

This might get a better answer on proofassistants.stackexchange. Regarding formalized mathematics in HoTT: people formalising mathematics in HoTT are typically interested in questions about higher types, which form a very small subset of pure mathematics. People formalising it in systems like Lean, Coq and Isabelle are typically interested in all of pure mathematics.

[Nick Dean]

Kevin Buzzard said:

This might get a better answer on proofassistants.stackexchange. Regarding formalized mathematics in HoTT: people formalising mathematics in HoTT are typically interested in questions about higher types, which form a very small subset of pure mathematics. People formalising it in systems like Lean, Coq and Isabelle are typically interested in all of pure mathematics.

Great, thanks Kevin (for the answer and the pointer)!

[Utensil Song]

Can't help to quote "lean-ness of Lean":

......the base language should be sufficiently expressive for the formalization of advanced mathematics and for program verification, for which dependent type theory seemed like the most promising foundation. Thus the lean-ness of Lean should be understood in comparison to other implementations of dependent type theory, which does come with a certain degree of fundamental complexity compared to simpler logic systems. Compared to Coq, whose type theory Lean’s is inspired by and still closest to, this in particular relates to replacing the primitive concepts of termination checking, fixpoint operators, and pattern matching with primitive recursor functions [Dybjer, 1994], as well as forgoing the type system-embedded module system.

from 1.3.3 The Essence of Lean in in An Extensible Theorem Proving Frontend ( @Sebastian Ullrich 's thesis ) .

[Utensil Song]

Another major change from Lean 2 was the removal of support for HoTT, which was done because of concerns over how to implement efficient tactics in the absence of proof irrelevance and the code duplication resulting from this as well as uncertainty at that time over whether “book HoTT” or the recent computational version of Cubical Type Theory [Cohen et al., 2015] was preferable.

from 1.3.4 A Short History of Lean

[Utensil Song]

Combining both paragraphs, my understanding is that Lean was looking for an appropriately lean foundation for Lean that provides sufficient support for the formalization of advanced mathematics and for program verification, and be able to write efficient tactics at the same time (thus requires proof irrelevance?).

Choosing its type theory foundation on a "lean" one also doesn't stop Lean to do research/formalization on HoTT or similar math branches, requiring no modification to Lean kernel.

[Nick Dean]

(deleted-duplicate response)

[Nick Dean]

Utensil Song said:

Combining both paragraphs, my understanding is that Lean was looking for an appropriately lean foundation for Lean that provides sufficient support for the formalization of advanced mathematics and for program verification, and be able to write efficient tactics at the same time (thus requires proof irrelevance?).

Choosing its type theory foundation on a "lean" one also doesn't stop Lean to do research/formalization on HoTT or similar math branches, requiring no modification to Lean kernel.

Ahhhh. Thanks a lot for your answers (and for including the poetic 'leanness of Lean'!). Clarified various things for me

[Kevin Buzzard]

I don't think that Leo had any interest at all in the formalisation of mathematics when he wrote Lean; I think that the fact that it is extensively used for formalisation of mathematics is little more than a very happy historical fluke (combined with the fact that it turned out to be a very powerful tool for formalising mathematics).

[Ioannis Konstantoulas]

Kevin Buzzard said:

I don't think that Leo had any interest at all in the formalisation of mathematics when he wrote Lean; I think that the fact that it is extensively used for formalisation of mathematics is little more than a very happy historical fluke (combined with the fact that it turned out to be a very powerful tool for formalising mathematics).

Ooh! What was the initial motivation?

[Jireh Loreaux]

If you want to hear about Leo's initial motivations and much more, this recent podcast is quite relevant: https://podcasts.google.com/feed/aHR0cHM6Ly93d3cudHlwZXRoZW9yeWZvcmFsbC5jb20vZXBpc29kZXMubXAzLnJzcw/episode/aHR0cHM6Ly93d3cudHlwZXRoZW9yeWZvcmFsbC5jb20vMjAyMy8wOS8wOS8zMy1MZW8tZGUtTW91cmEuaHRtbA?ep=14

[Siddhartha Gadgil]

One thing that Lean has thanks to a lack of legacy is pleasant unicode based notation. Also it can be used in VS Code which is an editor that riff-raff like myself can use easily.

[Mario Carneiro]

note that coq, agda, and isabelle also use unicode-based notation, it's not really a lean exclusive invention

[Mario Carneiro]

in fact, one of the common criticisms of agda is that people use way too much unicode

[Siddhartha Gadgil]

Mario Carneiro said:

note that coq, agda, and isabelle also use unicode-based notation, it's not really a lean exclusive invention

I see. I saw Gonthier's talk at the ICM and he used \Sigma. So I assumed this was what Coq forced.

[Siddhartha Gadgil]

Here I was not talking of Lean inventions, just the benefits of a lack of legacy so one can start with a world already having Javascript, LSP, Unicode etc.

[Mario Carneiro]

Most programming languages are unicode-capable these days

[Mario Carneiro]

but it is a common belief especially among programmers that unicode use is confusing and dangerous, or difficult to input, or both

[Mario Carneiro]

of course lean has a great IME for unicode but I'm not sure it has a great track record for avoiding confusables

[Eric Rodriguez]

it's quite annoying that often lean code gets flagged by the vscode unicode thing

[Yaël Dillies]

What's the "vscode unicode thing"?

[Eric Rodriguez]

image.png

[Shreyas Srinivas]

Siddhartha Gadgil said:

One thing that Lean has thanks to a lack of legacy is pleasant unicode based notation. Also it can be used in VS Code which is an editor that riff-raff like myself can use easily.

This might be more of a vim/emacs debate. Lean has a cultural edge in the math community, in the same way Coq has a userbase among the PL+verification community.

1. Lean's tooling is great and it has the sort of OSS culture where people jump on to the zulip server and collaborate. Since it is fairly new, it is easy to get changes implemented compared to a tool with a lot of older codebases and power users to support. It got onto the LSP bandwagon earlier compared to other ITPs for example.
2. I am guessing math people love that the lean community tries to accommodate their preferences as far as possible, rather than pontificating on how math ought to be done. Plus there's less backward compatibility to worry about.
3. It attracts programmers who are not necessarily mathematicians who like to contribute to the tooling, build system, tactics, as well as math stuff. If you ask power users of other ITPs, I am sure they'll give you really convincing arguments
4. The various parts of the system are more loosely coupled with each other. So while Coq has to maintain CoqIDE for each platform release and isabelle is tied to encoding choices made 20 years ago (whence their need to package their own vscodium which doesn't work with other up-to-date extensions), changes in the lean UX are less painful to make.

EDIT:

5. Lean has great learning material going for it: tpil, fpil, mpil, and most importantly the games. Coq's Software Foundations are great too, but more verification focussed than math focussed.

[Alex J. Best]

Eric Rodriguez said:

image.png

i've never seen that, does it show up for you in lean files, if you click adjust settings can you turn it off? (we could add this to the mathlib default settings if needed)

[Eric Rodriguez]

it may be turned off by default somehow? I've seen it pop up but rarely

[Patrick Massot]

The relevant settings are

"editor.unicodeHighlight.ambiguousCharacters": false,
"editor.unicodeHighlight.nonBasicASCII": false,

[Karl Palmskog]

Coq has to maintain CoqIDE for each platform release

For the record, CoqIDE is now in bugfix-only mode and is on its way out from the Coq GitHub repository. There are two VS Code extensions for Coq using novel language servers (developed outside Coq repo) supporting Isabelle-style interaction: VsCoq2 and Coq-LSP