How To Prove It with Lean

djvelleman.github.io/HTPIwL

This tutorial has the merit of actually trying you to do some meaningful mathematics before teaching you a billion items of syntax and dependent type theory nuances.

 Ancestors (8)

Lean bibliography
Lean (proof assistant)
List of proof assistants
Proof assistant
Formalization of mathematics
Area of mathematics
Mathematics
 Home