[HN Gopher] A Beginner's Companion to Theorem Proving in Lean 4
       ___________________________________________________________________
        
       A Beginner's Companion to Theorem Proving in Lean 4
        
       Author : PaulHoule
       Score  : 67 points
       Date   : 2024-01-06 12:26 UTC (10 hours ago)
        
 (HTM) web link (emallson.net)
 (TXT) w3m dump (emallson.net)
        
       | bertman wrote:
       | See also Terence Tao's blog posts detailing how he's using Lean
       | 4:
       | 
       | https://terrytao.wordpress.com/tag/lean4/
        
       | noqc wrote:
       | To the author, Lean is not mathlib (A fact that you will probably
       | get sick of hearing if you spend time in the zulip). If your
       | objective with lean is to use mathlib, you should try following
       | the mathlib tutorial as well.
        
       | dataangel wrote:
       | Assuming I did proofs in highschool algebra and geometry courses,
       | is there any tutorial that would make lean4 accessible? I think
       | computer assisted theorem proving could be great educationally,
       | but this post would be complete gobligook to most students
       | despite the title.
        
         | dunham wrote:
         | I enjoyed working through "Theorem Proving in Lean 4", although
         | it doesn't go deep into the mathematics side of things. I
         | intend to work through "Mathematics in Lean"[2] to get more
         | detail on that, but I want to finish "Programming Language
         | Foundations in Agda" first.
         | 
         | [1]: https://lean-lang.org/theorem_proving_in_lean4/
         | 
         | [2]: https://github.com/leanprover-
         | community/mathematics_in_lean
         | 
         | Edit: Oh, also the "Natural Number Game" is a nice, short intro
         | to the theorem proving that gets straight to the point:
         | https://adam.math.hhu.de/
        
         | qbit42 wrote:
         | This game is a decent introduction, though I think it has
         | plenty of room for improvement:
         | https://adam.math.hhu.de/#/g/leanprover-community/nng4.
        
         | mietek wrote:
         | Maybe try "Programming Language Foundations in Agda" instead.
         | 
         | https://plfa.github.io
        
         | anatnom wrote:
         | Check out the "Natural Number Game"[0], which is sort of a
         | practical tutorial but leaves a LOT of things unexplained. I
         | took a few proofs-heavy university classes among the
         | math/cs/philosophy departments so the idea of proving
         | arithmetic from axioms wasn't new, but the NNG still took me an
         | outrageous amount of time (easily 100 hours) and I got nowhere
         | near finishing. Perhaps I just never got things to click into
         | place; I am still profoundly confused about what the 'tactics'
         | truly are.
         | 
         | In my opinion, lean4 is not in any way "for beginners" as you
         | mean it; it is a tool for experts in mathematics.
         | 
         | [0] https://adam.math.hhu.de/#/g/leanprover-community/NNG4
        
         | theteapot wrote:
         | I think you should probably understand formal logic, and may
         | proof theory and also abstract algebra as a pre-req.
        
       ___________________________________________________________________
       (page generated 2024-01-06 23:01 UTC)