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
Honestly, I'd say just play some of the lean games instead (<a href="https://adam.math.hhu.de/" rel="nofollow">https://adam.math.hhu.de/). I went through the dependent type theory and proof stuff first, and in hindsight it would have been much faster to just get the intuition first from learning to use a language like lean.
Sure, use whatever method of learning that works well for you.
All I'm saying is that you're unlikely to be making effective use of a tool like this without understanding it's theoretical foundations.
I have absolutely no idea why you’re trying to make out that compactness for example is part of the theoretical foundations of Lean, but it definitely isn’t, and it’s so far off-base that I’m wondering why you’re saying things like this.
Compactness[1] is a useful property of some sets. It’s an example of the type of thing you might want to prove or disprove (eg that a certain set in a given metric space is or isn’t compact, or prove the Heine-Borel theorem or whatever), but if you’re not trying to do that, you can go about your merry way and learn a ton of lean without being aware that the concept of compactness even exists.
The same is true of incompleteness for example, which has literally never entered into the realm of being relevant for anything I’ve done in lean, and is definitely not in any way important prerequisite knowledge.
[1] And yes, I really do know what compactness is and I learned that the hard way by working on a bunch of proofs in analysis. There’s really no substitute for learning by doing. A set S is compact if and only if any open cover (ie family of open sets {T_i}_{i in I} such that the union U_{i in I} T_i is a superset of S for some possibly infinite indexing set I) contains a _finite_ subcover (a family {T_j}_{j in J} where J is a finite subset of I and the union over J of all the T_j’s also covers S). Compactness in logic is a consequence of compactness in the set-theoretic sense and really has no relevance whatsoever to lean.
I believe that compactness has a different meaning in topology than in logic btw (though my degree was so long ago now that I'm rusty on it all!).
I do find it implausible that you'd need the type of background that I had in logic back then, which included the type of stuff mentioned, for doing stuff in Lean though.
I use lean a lot, reasonably effectively (although I’m still just getting started) but I’m using it as a proof assistant for mathematics. The background that is actually useful for understanding how lean works and most “mathematical” lean use cases is dependent type theory and homotopy type theory. So people who really want to go deep on lean often recommend the HoTT book (<a href="https://homotopytypetheory.org/book/" rel="nofollow">https://homotopytypetheory.org/book/) but that’s not required reading for getting started in lean, more like if you’re doing a PhD in formalization or whatever.
It sounds like for your use case of software verification mathematical logic is important, but that’s definitely not the case for most lean users. I wouldn’t say it’s required or even useful if you want to use lean for proving things in general.
Most of my lean work involves software verification and transition systems. I suspect most people here would be interested in software verification rather than trying to solve unsolved math problems. You'd have a frustrating experience without the required logic background, from my experience dealing with a collaborator's new PhD students.
Or, you could invest time in making a tool that can be used effectively without having to understand all the theoretical foundations. What's stopping you?
You're crazy. Don't bother to try to understand lean's internal models unless you want to work on lean itself. Whatever style of proof you're used to, you can write in that style with mathlib.
What you actually need is knowledge of an overview of the Mathematics of Formal Methods in all their aspects viz. Predicate Logic, Set Theory, Temporal Logic, Type Systems etc.
Towards that end I highly recommend the following books;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke - An easy-to-read book needed for background mathematical fundamentals.
2) Understanding Formal Methods by Jean-Francois Monin - This gives an excellent overview of the core topics and a must-read. From here you can branch off into studying any specific approach and its tool (eg. Lean4/TLA+/etc.). Once you have studied this there is nothing "Formal" (specification/verification/etc.) which is impenetrable.
3) The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - Walks you through the entire process of deriving a program using successive refinements from specifications using Hoare/Dijkstra approach.
The above books do not need a math degree; You just need to become "familiar" with the mathematical form and its jargon. Most programmers can read and understand them.
You can easily finish the books in a couple of months using AI for clarifying/simplifying difficult concepts to gain quicker understanding.
AI can produce all the How but the What/Why still needs to happen in your head and hence the need to understand the mathematics.
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].
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
6gvONxR4sf7o · · focus · HN ↗
fooker · · focus · HN ↗
All I'm saying is that you're unlikely to be making effective use of a tool like this without understanding it's theoretical foundations.
seanhunter · · focus · HN ↗
Compactness[1] is a useful property of some sets. It’s an example of the type of thing you might want to prove or disprove (eg that a certain set in a given metric space is or isn’t compact, or prove the Heine-Borel theorem or whatever), but if you’re not trying to do that, you can go about your merry way and learn a ton of lean without being aware that the concept of compactness even exists.
The same is true of incompleteness for example, which has literally never entered into the realm of being relevant for anything I’ve done in lean, and is definitely not in any way important prerequisite knowledge.
[1] And yes, I really do know what compactness is and I learned that the hard way by working on a bunch of proofs in analysis. There’s really no substitute for learning by doing. A set S is compact if and only if any open cover (ie family of open sets {T_i}_{i in I} such that the union U_{i in I} T_i is a superset of S for some possibly infinite indexing set I) contains a _finite_ subcover (a family {T_j}_{j in J} where J is a finite subset of I and the union over J of all the T_j’s also covers S). Compactness in logic is a consequence of compactness in the set-theoretic sense and really has no relevance whatsoever to lean.
jvvw · · focus · HN ↗
I do find it implausible that you'd need the type of background that I had in logic back then, which included the type of stuff mentioned, for doing stuff in Lean though.
seanhunter · · focus · HN ↗
fooker · · focus · HN ↗
If you want to master it and use it effectively for something real, yeah some reading would help.
seanhunter · · focus · HN ↗
It sounds like for your use case of software verification mathematical logic is important, but that’s definitely not the case for most lean users. I wouldn’t say it’s required or even useful if you want to use lean for proving things in general.
fooker · · focus · HN ↗
Math is full of fun overloads like this.
Most of my lean work involves software verification and transition systems. I suspect most people here would be interested in software verification rather than trying to solve unsolved math problems. You'd have a frustrating experience without the required logic background, from my experience dealing with a collaborator's new PhD students.
watt · · focus · HN ↗
fooker · · focus · HN ↗
If someone would figure this out, the theoretical advancements they would discover on the way would likely earn them a Turing award.
thaumasiotes · · focus · HN ↗
fooker · · focus · HN ↗
Yes, you can do that, and it'll be a frustrating experience.
Knowing the theoretical foundations of your tool is a great way to be happy and productive.
Without it you have issues similar to people trying to implement parsers with regex. :)
rramadass · · focus · HN ↗
Towards that end I highly recommend the following books;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke - An easy-to-read book needed for background mathematical fundamentals.
2) Understanding Formal Methods by Jean-Francois Monin - This gives an excellent overview of the core topics and a must-read. From here you can branch off into studying any specific approach and its tool (eg. Lean4/TLA+/etc.). Once you have studied this there is nothing "Formal" (specification/verification/etc.) which is impenetrable.
3) The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - Walks you through the entire process of deriving a program using successive refinements from specifications using Hoare/Dijkstra approach.
whattheheckheck · · focus · HN ↗
I thought this AI or SI was supposed to make shit easier for everyone.
fooker · · focus · HN ↗
rramadass · · focus · HN ↗
The above books do not need a math degree; You just need to become "familiar" with the mathematical form and its jargon. Most programmers can read and understand them.
You can easily finish the books in a couple of months using AI for clarifying/simplifying difficult concepts to gain quicker understanding.
AI can produce all the How but the What/Why still needs to happen in your head and hence the need to understand the mathematics.
Dashadower · · focus · HN ↗
uptodatenews · · focus · HN ↗
<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...
auggierose · · focus · HN ↗
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
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.