Yes, this is very old. This is a review of Lean 3; Lean 4 is about to appear and this deals with several of the issues flagged by Hales, for example speed.
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.
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.
The Lean developers put out a paper about v4's reference counting last year which shows that in basic benchmarks, Lean 4 is in the same ballpark as Haskell, Swift, and ML. https://arxiv.org/abs/1908.05647
>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?
11 comments
[ 4.7 ms ] story [ 38.2 ms ] threadBuzzard’s wider Xena project is formalizing a huge chunk of the undergraduate-level math curriculum into a “standard library” of math, written in Lean.
[0] https://leanprover-community.github.io/lt2021/
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?