lean tutorials

lean tutorials

lean quick start https://lean-lang.org/lean4/doc/quickstart.html

lean intro and setup.

• • Theorem Proving in Lean 4
  • 2025-02-11
  • By Jeremy Avigad, Leonardo De Moura, Soonho Kong And Sebastian Ullrich.
  • https://lean-lang.org/theorem_proving_in_lean4/

• Difficult to read.
• Covers lean as proof system, its mechanism as a programing language.
• dense.
• chapter 2 covers type theory basics, dense.

• Math in Lean
• 2020
• By Jeremy Avigad, Patrick Massot.
• https://leanprover-community.github.io/mathematics_in_lean/index.html

• The Mechanics of Proof
• 2024
• By Heather Macbeth.
• https://hrmacbeth.github.io/math2001/

difficult to read

• The Lean Language Reference https://lean-lang.org/doc/reference/latest/

bad tutorial

• Functional Programming in Lean
• 2023
• By David Thrane Christiansen.
• https://lean-lang.org/functional_programming_in_lean/