Lean Proof Assistant
Lean Proof Assistant.
- from
- Theoretical Computer Science
- added
- 2026-10-10
- likes
- 0
similar
-
Lean lean-lang.org
Open-source interactive theorem prover and programming language based on dependent type theory, used for formal mathematics and software verification.
-
Theorem Proving in Lean 4 lean-lang.org
Free official textbook on dependent type theory, propositions, tactics, inductive types, type classes, and constructing verified proofs in Lean 4.
-
mathlib github.com
Community-maintained mathematical library for Lean 4, with formalized theories, proof tactics, programming infrastructure, and generated documentation.
-
Mathematics in Lean leanprover-community.github.io
Free textbook with examples and exercises for mathematicians learning Lean 4 and mathlib.
-
Courses Using Lean leanprover-community.github.io
Maintained, filterable index of university courses that teach Lean or use it for mathematics, logic, programming, and formal verification.
-
LeanDojo v2 leandojo.org
Open-source framework and benchmark data for training, evaluating, and deploying AI-assisted theorem provers for Lean 4.
Theoretical Computer Science › Formal Verification > Books: “Lean Proof Assistant.”