A Review of the Lean Theorem Prover

For reference, a great intro to Lean for programmer-types without an academic maths background is Kevin Buzzard’s Natural Number Game: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...

Buzzard’s wider Xena project is formalizing a huge chunk of the undergraduate-level math curriculum into a “standard library” of math, written in Lean.

>Lean makes it easy to switch from constructive to classical logic (you just open the classical logic module).

I wonder what this is in comparison to. Coq also has a classical logic module (though it is more awkwardly named). HOL Light is, from a quick Google, already a classical prover. Are there any provers where classical logic is hard to come by? Or is Coq's version more complicated to use?

>Lean makes quotient types easy (unlike Coq, when tends to work with awkward setoids).

(At the cost of subject reduction). This remains the most interesting point of comparison in my mind. How can the Lean kernel be sound if it's possible to reduce proofs to non-proofs?

>.... it is nearly impossible in Lean to curry a structure. That is, what is bundled cannot be later opened up as a parameter.

Could a Lean user shed some more light on this? In what circumstances would you want to treat a bundled type as a parameter? Surely accessing the type itself - like the underlying set of a group, in the example - can still be done in either case?

Related for people into provers, there is a set of notes here https://cs.uwaterloo.ca/~plragde/842/handouts/notes.html to help you work through the Agda book https://plfa.github.io/ which is done using emacs, atom or vscode

From the perspective of this software engineer, Lean seems mostly superior to the other proof assistant languages. You can develop in a regular text editor, the source code is open, you don’t have any hacky “some expressions are a sublanguage in string constants” stuff, and most importantly the community is extremely responsive. Speed is the biggest problem; Lean 3 still has a very slow interpreter and it makes some things (in particular communicating out to an external specialized solver like the “hammer” tactics) too slow to be practical. If Lean 4 manages to improve speed as much as promised, and the 3 -> 4 migration actually happens, I think it will become the all-around superior choice.

Stumpled upon Lean on YT this morning. Coincidence or anything new upcoming?

2018