Mathematics Resources for learning Lean (4) Lean 4 manual Theorem proving in Lean 4 Functional programming in Lean 4