Lean-4-Literature

A curated list of Lean 4 literature.

Beginner friendly

1. Theorem Proving in Lean 4 - Use Lean 4 as a proof assistant to prove theorems.
2. Functional Programming in Lean - Use Lean 4 as a programming language.
3. The Mechanics of Proof - Use Lean 4 to do 'common' mathematics.
4. The Hitchhiker's Guide to Logical Verification - Use Lean 4 to do 'common' computer science.

Intermediate and onwards

1. Metaprogramming in Lean 4 - Extend Lean 4 with custom functionality.
2. Type Checking in Lean 4 - Learn about Lean 4 metatheory.
3. Scientific Computing in Lean - WIP - Modern approach to scientific computing melding convenience of use, correctness, and performance.