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

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/