# References

## Official Documentation

- [Lean 4 Manual](https://lean-lang.org/lean4/doc/)
- [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/)
- [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
- [Metaprogramming in Lean 4](https://leanprover-community.github.io/lean4-metaprogramming-book/)
- [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/)
- [Mathlib Documentation](https://leanprover-community.github.io/mathlib4_docs/)
- [Lean Zulip Chat](https://leanprover.zulipchat.com/)

## Theorem Proving Games

- [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4) - HHU Düsseldorf
- [Real Analysis Game](https://adam.math.hhu.de/#/g/AlexKontorovich/RealAnalysisGame) - Rutgers University
- [Reintroduction to Proofs](https://adam.math.hhu.de/#/g/emilyriehl/ReintroductionToProofs) - 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](https://github.com/emilyriehl/ReintroductionToProofs)

## University Courses (Lean 4)

- [Functional Programming and Theorem Proving](https://web.stanford.edu/class/cs99/) - Stanford University
- [Formal Proof and Verification](https://browncs1951x.github.io/) - Brown University
- [The Mechanics of Proof](https://hrmacbeth.github.io/math2001) - Fordham University
- [Formalising Mathematics](https://github.com/ImperialCollegeLondon/formalising-mathematics-2024) - Imperial College London
- [Formalized Mathematics in Lean](https://github.com/fpvandoorn/LeanCourse24) - University of Bonn
- [Interactive Theorem Proving](https://www.tcs.ifi.lmu.de/lehre/ss-2024/itp_de.html) - LMU Munich
- [Proofs and Programs](http://math.iisc.ac.in/~gadgil/proofs-and-programs-2025/) - Indian Institute of Science
- [Theorem Proving with Lean](https://adomani.github.io/Syllabus/MA4N1/toc) - University of Warwick
- [Logic and Mechanized Reasoning](https://avigad.github.io/lamr/) - Carnegie Mellon University
- [Lean for Scientists and Engineers](https://github.com/ATOMSLab/LFSE2024/) - University of Maryland
- [An Introduction to Lean 4](https://www.uv.es/coslloen/Lean4/) - Universitat de València
- [Interactive Theorem Proving in Lean](https://matematiflo.github.io/LeanCompactCourse/) - MPI Leipzig
- [The Hitchhiker's Guide to Logical Verification](https://github.com/lean-forward/logical_verification_2025) - Various institutions
- [Formal Methods in Mathematics](https://elo.mastermath.nl/course/info.php?id=1121) - Mastermath (Netherlands)
- [Logique et démonstrations assistées](https://www.imo.universite-paris-saclay.fr/~patrick.massot/enseignement/) - Université Paris-Saclay
- [Semantics and Verification of Software](https://moves.rwth-aachen.de/teaching/ws-2024-25/savos/) - RWTH Aachen
- [Formal Proof](https://github.com/math4345) - Ohio State University
- [Lean Community Course Catalog](https://github.com/leanprover-community/leanprover-community.github.io/blob/lean4/data/courses.yaml) - Full listing

## University Courses (Lean 3)

- [Logic and Proof](https://lean-lang.org/logic_and_proof/) - Carnegie Mellon University
- [Modern Mathematics with Lean](https://gihanmarasingha.github.io/modern-maths-pages/) - University of Exeter
- [Graduate Introduction to Logic](https://math.hawaii.edu/wordpress/bjoern/math-654-fall-2022/) - University of Hawaii
- [Introduction to Proofs with Lean](https://sinhp.github.io/teaching/2022-introduction-to-proofs-with-Lean) - Johns Hopkins University
- [Logic and Modelling](https://studiegids.vu.nl/en/2022-2023/courses/X_401015) - Vrije Universiteit Amsterdam
- [Harvard MATH 161](https://beta.my.harvard.edu/course/MATH161/2026-Spring/001) - University course on theorem proving with Lean and Mathlib.