Tutorials
These tutorials cover version 4.29.0-nightly-2026-02-05 of Lean. While the reference manual describes the system and its features in detail, these tutorials provide focused introductions to specific tools.
Tactics
These tutorials demonstrate Lean's advanced proof automation.
- Verifying Imperative Programs Using
mvcgen A demonstration of how to use Lean's verification condition generator to conveniently and compositionally prove properties of monadic programs.
- Using
grindfor Ordered Maps A demonstration of how to use
grindto automate essentially all proofs in a new data structure. The resulting API finds proofs automatically, allowing code that is both safe and convenient.