Tutorials
These tutorials cover version 4.27.0-rc1 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.