4 ms·

A Review of the Lean Theorem Prover

67 points by oli5679 6y ago

alimw 6y ago
2018
- kevinbuzzard 6y ago
  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.
trevyn 6y ago
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_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.
- oli5679 6y ago
  this is great, thanks!
peheje 6y ago
Stumpled upon Lean on YT this morning. Coincidence or anything new upcoming?
- mauricioc 6y ago
  Probably a coincidence, but also Lean Together 2021 [0] is happening next week and it is likely that many Lean 4 details will be revealed there. [0] https://leanprover-community.github.io/lt2021/ https://leanprover-community.github.io/lt2021/
lacker 6y ago
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.
- mcguire 6y ago
  From the perspective of this software engineer, "the 3 -> 4 migration actually happens" was the part of the article that was most disappointing.
- lakecresva 6y ago
  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 https://arxiv.org/abs/1908.05647
ivanbakel 6y ago
>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?
rithmAlgo 6y ago
Related for people into provers, there is a set of notes here https://cs.uwaterloo.ca/~plragde/842/handouts/notes.html https://cs.uwaterloo.ca/~plragde/842/handouts/notes.html to help you work through the Agda book https://plfa.github.io/ https://plfa.github.io/ which is done using emacs, atom or vscode

67 points by oli5679 6y ago

alimw 6y ago

2018

kevinbuzzard 6y ago
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.

trevyn 6y ago

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_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.

oli5679 6y ago
this is great, thanks!

peheje 6y ago

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

mauricioc 6y ago
Probably a coincidence, but also Lean Together 2021 [0] is happening next week and it is likely that many Lean 4 details will be revealed there. [0] https://leanprover-community.github.io/lt2021/ https://leanprover-community.github.io/lt2021/

lacker 6y ago

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.

mcguire 6y ago
From the perspective of this software engineer, "the 3 -> 4 migration actually happens" was the part of the article that was most disappointing.
lakecresva 6y ago
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 https://arxiv.org/abs/1908.05647

ivanbakel 6y ago

>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?

rithmAlgo 6y ago

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