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
This is absolutely not a helpful list for someone who wants to prove things in lean, and just seems like weird gate-keeping. In particular, Proof Trees are completely irrelevant, incompleteness and compactness are only relevant if you are proving things in those specific fields and the only thing you need to know about constructive vs intuitionistic vs classical logic in lean is if you want to use the law of the excluded middle or some non-constructive proofs and tactics, lean won’t force that on you, so you sometimes need to “open classical”. (And this is covered in “Mathematics in Lean” and “Theorem Proving in Lean” at the appropriate place).
Knowing that the Curry-Howard correspondence exists is important if you care about the CS magic that makes lean work and to understand how term mode and tactic mode relate to each other but again it’s really not necessary to understand the correspondence itself to use lean as a proof assistant. (And this is covered extensively in “Theorem proving in Lean” if that’s your jam).
Whatever mathematical background you have is obviously helpful and will widen the scope of what you can do, but you don’t need to learn a huge amount of foundational mathematics to get your hands dirty in lean. For example, “The Mechanics of Proof” by Heather Macbeth was written as a course for 1st year undergrads so only assumes high school maths knowledge. Here’s a list of learning resources that the lean prover community recommends <a href="https://leanprover-community.github.io/learn.html" rel="nofollow">https://leanprover-community.github.io/learn.html
One thing I would add is if you want to learn about proof writing in general there are a lot of good resources out there including “The Book of Proof” which is free online. <a href="https://rcsnyder.github.io/open-frontier-curriculum/07-resources/textbooks/mathematical-reasoning/" rel="nofollow">https://rcsnyder.github.io/open-frontier-curriculum/07-resou...
I personally really enjoyed Jay Cummings’ “Proof: A long-form mathematics textbook” which is on that list as it provides lovely little intros to various areas of mathematics along the way. I have done every exercise in that book and had a lot of fun in the process.
But these aren’t things you necessarily need to do before getting started in lean.
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
seanhunter · · focus · HN ↗
Knowing that the Curry-Howard correspondence exists is important if you care about the CS magic that makes lean work and to understand how term mode and tactic mode relate to each other but again it’s really not necessary to understand the correspondence itself to use lean as a proof assistant. (And this is covered extensively in “Theorem proving in Lean” if that’s your jam).
Whatever mathematical background you have is obviously helpful and will widen the scope of what you can do, but you don’t need to learn a huge amount of foundational mathematics to get your hands dirty in lean. For example, “The Mechanics of Proof” by Heather Macbeth was written as a course for 1st year undergrads so only assumes high school maths knowledge. Here’s a list of learning resources that the lean prover community recommends <a href="https://leanprover-community.github.io/learn.html" rel="nofollow">https://leanprover-community.github.io/learn.html
One thing I would add is if you want to learn about proof writing in general there are a lot of good resources out there including “The Book of Proof” which is free online. <a href="https://rcsnyder.github.io/open-frontier-curriculum/07-resources/textbooks/mathematical-reasoning/" rel="nofollow">https://rcsnyder.github.io/open-frontier-curriculum/07-resou...
I personally really enjoyed Jay Cummings’ “Proof: A long-form mathematics textbook” which is on that list as it provides lovely little intros to various areas of mathematics along the way. I have done every exercise in that book and had a lot of fun in the process.
But these aren’t things you necessarily need to do before getting started in lean.