4 ms·

Assuming I did proofs in highschool algebra and geometry courses, is there any tutorial that would make lean4 accessible? I think computer assisted theorem prov

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 3y ago
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/ https://lean-lang.org/theorem_proving_in_lean4/ [2]: https://github.com/leanprover-community/mathematics_in_lean 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/ https://adam.math.hhu.de/
qbit42 3y ago
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 https://adam.math.hhu.de/#/g/leanprover-community/nng4.
mietek 3y ago
Maybe try “Programming Language Foundations in Agda” instead. https://plfa.github.io https://plfa.github.io
anatnom 3y ago
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 https://adam.math.hhu.de/#/g/leanprover-community/NNG4
- mcshicks 3y ago
  I absolutely agree that it's not for beginners, but amateurs can still have fun. I did the NNG in lean 3 and again lean 4. It didn't take me 100s of hours but I've also spent a lot of time over the last decade trying to brush up my math skills. One of the main problems with proofs is other than having a mathematician friend who's willing to check its really hard to know if you did it correctly. My son is a mathematician and I still didn't want to ask him to check my proofs! The cool thing for me about lean is I can do some form of math proofs and not have to ask somebody if I got it right. If you liked that you might like the natural set game as well. https://adam.math.hhu.de/#/g/djvelleman/stg4 https://adam.math.hhu.de/#/g/djvelleman/stg4 The author of the math book "How to Prove it" Daniel Velleman who I think did the set game also has a "How to Prove it with Lean" which is nice because the exercises correlate to the book. https://djvelleman.github.io/HTPIwL/ https://djvelleman.github.io/HTPIwL/ I've found the lean community on zulip really open to amateurs to want to learn. I asked what I considered a "duh" type of question once I saw the answer, and the guy that helped me is kind of "the lean math" guy. https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/
- nyssos 3y ago
  > I am still profoundly confused about what the 'tactics' truly are. They're macros: a `tactic a` is (after sanding off the implementation details) a function tactic_state -> Either (tactic_state, error) (tactic_state, a) where `tactic_state` is the internal state of the elaborator.
theteapot 3y ago
I think you should probably understand formal logic, and may proof theory and also abstract algebra as a pre-req.

dunham 3y ago

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/ https://lean-lang.org/theorem_proving_in_lean4/ [2]: https://github.com/leanprover-community/mathematics_in_lean 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/ https://adam.math.hhu.de/

qbit42 3y ago

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 https://adam.math.hhu.de/#/g/leanprover-community/nng4.

mietek 3y ago

Maybe try “Programming Language Foundations in Agda” instead. https://plfa.github.io https://plfa.github.io

anatnom 3y ago

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 https://adam.math.hhu.de/#/g/leanprover-community/NNG4

mcshicks 3y ago
I absolutely agree that it's not for beginners, but amateurs can still have fun. I did the NNG in lean 3 and again lean 4. It didn't take me 100s of hours but I've also spent a lot of time over the last decade trying to brush up my math skills. One of the main problems with proofs is other than having a mathematician friend who's willing to check its really hard to know if you did it correctly. My son is a mathematician and I still didn't want to ask him to check my proofs! The cool thing for me about lean is I can do some form of math proofs and not have to ask somebody if I got it right. If you liked that you might like the natural set game as well. https://adam.math.hhu.de/#/g/djvelleman/stg4 https://adam.math.hhu.de/#/g/djvelleman/stg4 The author of the math book "How to Prove it" Daniel Velleman who I think did the set game also has a "How to Prove it with Lean" which is nice because the exercises correlate to the book. https://djvelleman.github.io/HTPIwL/ https://djvelleman.github.io/HTPIwL/ I've found the lean community on zulip really open to amateurs to want to learn. I asked what I considered a "duh" type of question once I saw the answer, and the guy that helped me is kind of "the lean math" guy. https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/
nyssos 3y ago
> I am still profoundly confused about what the 'tactics' truly are. They're macros: a `tactic a` is (after sanding off the implementation details) a function tactic_state -> Either (tactic_state, error) (tactic_state, a) where `tactic_state` is the internal state of the elaborator.

theteapot 3y ago

I think you should probably understand formal logic, and may proof theory and also abstract algebra as a pre-req.