resources

LEAN Interactive Theorem Proving

Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types.

Repos

• https://github.com/leanprover/lean4
• https://github.com/leanprover/cslib/
• https://github.com/leanprover-community/mathlib4
• https://github.com/avigad
• https://github.com/lecopivo/SciLean

Websites

• https://lean-lang.org/
• https://lean-lang.org/doc/reference/latest/
• https://lean-lang.org/functional_programming_in_lean/

• https://lean-lang.org/theorem_proving_in_lean4/

• https://leanprover-community.github.io/
• https://leanprover-community.github.io/index.html
• https://leanprover-community.github.io/mathematics_in_lean/

• https://leanprover-community.github.io/100.html

• https://github.com/RobertoZunino/ITPCourse
• https://leanprover-community.github.io/learn.html (START HERE)

Chat

• https://leanprover.zulipchat.com/

Books

• https://lakesare.brick.do/all-lean-books-and-where-to-find-them-x2nYwjM3AwBQ
• https://github.com/blanchette/interactive_theorem_proving_2026
• https://leanprover-community.github.io/logic_and_proof/
• https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/manual/manual.md

Videos

• https://lean-forward.github.io/logical-verification/2022/index.html

• Big Conjectures

  Thomas Hales - https://www.youtube.com/playlist?list=PLgBHexwnIcdtfrvQB1xhCV2MgsmquyD-S

• Buzzard
  • https://www.youtube.com/@PietroMonticone/videos

  • Can AI Do Mathematics?

    Kevin Buzzard https://www.youtube.com/watch?v=O0F6EFyDA58

Tutorials

• https://github.com/pitmonticone/LeanInVienna2024

Awesome lists

https://github.com/fpvandoorn/lean-links

Papers

• CSLib: The Lean Computer Science Library