Theorem Proving in Lean 4
Free official textbook on dependent type theory, propositions, tactics, inductive types, type classes, and constructing verified proofs in Lean 4.
- from
- Math
- 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.
-
-
Mathematics in Lean leanprover-community.github.io
Free textbook with examples and exercises for mathematicians learning Lean 4 and mathlib.
-
mathlib github.com
Community-maintained mathematical library for Lean 4, with formalized theories, proof tactics, programming infrastructure, and generated documentation.
-
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.
-
Bengt. Programming in Martin-Löf's Type Theory cse.chalmers.se
This book describes different type theories (theories of types, polymorphic and monomorphic sets, and subsets) from a computing science perspective.
Math › Foundations and Logic > Formal Mathematics and Theorem Proving: “Free official textbook on dependent type theory, propositions, tactics, inductive types, type classes, and constructing verified proofs in Lean 4.”