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