We are currently updating the Lean community website to describe working with Lean 4, but most of the information you will find here today still describes Lean 3.

Pull requests updating this page for Lean 4 are very welcome. There is a link at the bottom of this page.

Please visit the leanprover zulip and ask for whatever help you need during this transitional period!

The website for Lean 3 has been archived. If you need to link to Lean 3 specific resources please link there.

Mathlib statistics


Definitions Theorems Contributors
67397 124629 310

Code growth

Temporal distribution


Dependency graph

A visualization showing how the various topics in mathlib interact and their relative sizes can be found here.