References

Official Documentation

• Lean 4 Manual
• Theorem Proving in Lean 4
• Functional Programming in Lean
• Metaprogramming in Lean 4
• Mathematics in Lean
• Mathlib Documentation
• Lean Zulip Chat

Theorem Proving Games

• Natural Number Game - HHU Düsseldorf
• Real Analysis Game - Rutgers University
• Reintroduction to Proofs - A game introducing proofs, dependent type theory, and Lean prepared by Emily Riehl for a first year seminar at Johns Hopkins (Fall 2025). Covers types, functions, products, coproducts, quantifiers, and dependent types through interactive puzzles. Source

University Courses (Lean 4)

• Functional Programming and Theorem Proving - Stanford University
• Formal Proof and Verification - Brown University
• The Mechanics of Proof - Fordham University
• Formalising Mathematics - Imperial College London
• Formalized Mathematics in Lean - University of Bonn
• Interactive Theorem Proving - LMU Munich
• Proofs and Programs - Indian Institute of Science
• Theorem Proving with Lean - University of Warwick
• Logic and Mechanized Reasoning - Carnegie Mellon University
• Lean for Scientists and Engineers - University of Maryland
• An Introduction to Lean 4 - Universitat de València
• Interactive Theorem Proving in Lean - MPI Leipzig
• The Hitchhiker’s Guide to Logical Verification - Various institutions
• Formal Methods in Mathematics - Mastermath (Netherlands)
• Logique et démonstrations assistées - Université Paris-Saclay
• Semantics and Verification of Software - RWTH Aachen
• Formal Proof - Ohio State University
• Lean Community Course Catalog - Full listing

University Courses (Lean 3)

• Logic and Proof - Carnegie Mellon University
• Modern Mathematics with Lean - University of Exeter
• Graduate Introduction to Logic - University of Hawaii
• Introduction to Proofs with Lean - Johns Hopkins University
• Logic and Modelling - Vrije Universiteit Amsterdam
• Harvard MATH 161 - University course on theorem proving with Lean and Mathlib.