Lean
Open-source interactive theorem prover and programming language based on dependent type theory, used for formal mathematics and software verification.
- from
- Math
- added
- 2026-10-10
- likes
- 0
similar
-
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.
-
-
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.
-
Mathematics in Lean leanprover-community.github.io
Free textbook with examples and exercises for mathematicians learning Lean 4 and mathlib.
-
LeanDojo v2 leandojo.org
Open-source framework and benchmark data for training, evaluating, and deploying AI-assisted theorem provers for Lean 4.
-
Lean-related Conferences and Events leanprover-community.github.io
Maintained calendar and archive of conferences, workshops, and tutorials about Lean, mathlib, and formalized mathematics.
Math › Foundations and Logic > Formal Mathematics and Theorem Proving: “Open-source interactive theorem prover and programming language based on dependent type theory, used for formal mathematics and software verification.”