Home

This is a Lean 4 walkthrough of exercises found in these materials:

• Kevin Buzzard, Natural Number Game
• Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich, Theorem Proving in Lean 4
• David Thrane Christiansen, Functional Programming in Lean
• Benjamin C. Pierce et al., Software Foundations
• Adam Chlipala, Certified Programming with Dependent Types
• Adam Chlipala, Formal Reasoning About Programs
• Yves Bertot and Pierre Castéran, Coq'Art
• Jeremy Avigad et al., Logic and Proof
• Jasmin Blanchette et al., Hitchhiker's Guide to Logical Verification
• Tobias Nipkow and Gerwin Klein, Concrete Semantics