One canonical definition per concept, so every problem in an area is stated in the same vocabulary rather than restating the mathematics. Definitions only — theorems and conjectures live with the problems that use them.

Search by Lean name or by meaning; every identifier links to where it is defined. Adapted with thanks from Mathlib, cslib and formal-conjectures, all Apache 2.0 — credits.