Please do not try to understand Lean or proof assistants without first getting a rudimentary understanding of the logic involved. This article sort of skips over it, which is reasonable because it is pretty involved.
Even if you have written a large number of math proofs, you'd usually not have learnt the language or logic of proofs themselves. And even if you are an accomplished computer scientist, logic is not just AND, OR, NOT.
Here is some necessary reading, feel free to find better sources but wikipedia is good too.
* Proof trees - <a href="https://en.wikipedia.org/wiki/Method_of_analytic_tableaux" rel="nofollow">https://en.wikipedia.org/wiki/Method_of_analytic_tableaux
IMO the experience of learning to use and understand a proof assistant gives one a pretty good foundation for then going deeper into logic and proof theory. I'm specifically thinking of Logical Foundations [0], which doubles as an introduction to Rocq and also an introduction to intuitionistic logic (and also type theory!).
Some specific disagreements:
- "Proof trees" on Wikipedia redirects to the page for analytic tableaus, which I don't think is particularly relevant to Lean. I think natural deduction [1] would be infinitely more useful.
- Why is Gödel incompleteness necessary for one to understand how Lean works?
- Why is compactness necessary knowledge? In my experience, one can use and understand any modern proof assistant without knowing anything about model theory.
[0] <a href="https://softwarefoundations.cis.upenn.edu/lf-current/index.html" rel="nofollow">https://softwarefoundations.cis.upenn.edu/lf-current/index.h..., and see also its sequel Programming Language Foundations [1].
fooker · · focus · HN ↗
Even if you have written a large number of math proofs, you'd usually not have learnt the language or logic of proofs themselves. And even if you are an accomplished computer scientist, logic is not just AND, OR, NOT.
Here is some necessary reading, feel free to find better sources but wikipedia is good too.
* Proof trees - <a href="https://en.wikipedia.org/wiki/Method_of_analytic_tableaux" rel="nofollow">https://en.wikipedia.org/wiki/Method_of_analytic_tableaux
* Constructive/Intuitionistic logic - <a href="https://en.wikipedia.org/wiki/Intuitionistic_logic" rel="nofollow">https://en.wikipedia.org/wiki/Intuitionistic_logic
* Proofs and Types - <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow">https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
* (In)completeness - <a href="https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems" rel="nofollow">https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
* Compactness - <a href="https://en.wikipedia.org/wiki/Compactness_theorem" rel="nofollow">https://en.wikipedia.org/wiki/Compactness_theorem
BalinKing · · focus · HN ↗
Some specific disagreements:
- "Proof trees" on Wikipedia redirects to the page for analytic tableaus, which I don't think is particularly relevant to Lean. I think natural deduction [1] would be infinitely more useful.
- Why is Gödel incompleteness necessary for one to understand how Lean works?
- Why is compactness necessary knowledge? In my experience, one can use and understand any modern proof assistant without knowing anything about model theory.
[0] <a href="https://softwarefoundations.cis.upenn.edu/lf-current/index.html" rel="nofollow">https://softwarefoundations.cis.upenn.edu/lf-current/index.h..., and see also its sequel Programming Language Foundations [1].
[1] <a href="https://softwarefoundations.cis.upenn.edu/plf-current/index.html" rel="nofollow">https://softwarefoundations.cis.upenn.edu/plf-current/index....
[1] <a href="https://en.wikipedia.org/wiki/Natural_deduction" rel="nofollow">https://en.wikipedia.org/wiki/Natural_deduction