CSE 290Q: Topics in Interactive Theorem Provers

This is a repository to organize materials for the Spring 2025 offering of CSE 290Q, which focuses on interactive theorem provers, with a strong focus on Lean.

How to get started:

1. https://docs.lean-lang.org/lean4/doc/quickstart.html
2. Run lake exe cache get to download a pre-built Mathlib
3. In VS Code, open the root cse-290q-25sp folder.

You may consider installing the Error Lens VS Code extension. I don't usually use it, but I enable it when doing live coding.

VS Code tip: on the "Lean Infoview" panel, click the "..." and select "Lock Group". This prevents this panel from being used when files are opened.

Resources

• Hitchhiker's Guide to Logical Verification https://github.com/lean-forward/logical_verification_2025
• Theorem Proving in Lean 4 https://lean-lang.org/theorem_proving_in_lean4/
• The Mechanics of Proof https://hrmacbeth.github.io/math2001/index.html
• The Natural Number Game https://adam.math.hhu.de/
• Functional Programming in Lean https://lean-lang.org/functional_programming_in_lean/
• Mathematics in Lean https://leanprover-community.github.io/mathematics_in_lean/
• Metaprogramming in Lean https://github.com/arthurpaulino/lean4-metaprogramming-book
• Homotopy Type Theory https://homotopytypetheory.org/book/
• Type Checking in Lean 4 https://ammkrn.github.io/type_checking_in_lean4/