The Lean theorem prover is a proof assistant developed principally by Leonardo de Moura.
The community is currently in the middle of switching from using Lean 3 to using Lean 4. This website is still being updated, and some pages have outdated information about Lean 3 (these pages are marked with a prominent banner). The old Lean 3 community website has been archived .
The Lean mathematical library, mathlib , is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. The library also contains definitions useful for programming. This project is very active, with many regular contributors and daily activity.
Matryoshka: Fast Interactive Verification through Strong Higher-Order Automation