This is a collection of resources to learn LEAN. This readme file contains descriptions, while the rest of the repository contains folders containing the other projects.
- Mathematics in LEAN - A mathematics focussed introduction to LEAN, covering things from Logic and Set Theory to Topology and Differential Calculus
- Downloadable PDF
- It also has an associated collection of exercises, the accompanying repository is within
mathematics_in_lean- build instructions
- The Hitchhiker's Guide to Logical Verification - A more computer science oriented introduction to LEAN, with a great deal of elaboration on the type theoretic foundations of LEAN
- Downloadable PDF
- It also has an associated collection of exercises, the accompanying repository is within
logical_verification_2023- (build instructions same as above)
- Loogle - A search engine that helps you search for theorems defined in LEAN's libraries, similar to how the Search command works in the Rocq theorem prover.
- Theorem Proving in LEAN4 - A general introduction to the LEAN theorem prover, assumes no specific background of the reader. One downside is that it does not have interactive exercises like the other books, however, it still works as a good reference.