Every result in the library is machine-checked: no
sorry, no admitted lemma, no axiom beyond the three Lean itself assumes.
This is the map of what is proved and what each proof rests on.
Five chains carry the library. Each arrow is a real dependency — the
target could not be stated or proved without the source. Solid nodes are verified;
the dashed frontier is what is not yet proved.
Lanes 1–4 are complete and kernel-checked. Lane 5 is the
live frontier: the translation estimate, the mollification rate, and the disjoint cell
lattice are proved, and the two compactness theorems they feed are not. The dashed
cross-links carry results between chains — density transfers a smooth-function
inequality to weak derivatives, and the Poincaré lane supplies the ∫|∇u|
term the De Giorgi isoperimetric argument consumes.
Explorer
Every module and what it rests on
Each dot is a module, placed left-to-right by how deep its dependency
chain runs and grouped by area. Click one to see its theorems and light up everything
it depends on, transitively.
Areas
Reading the map
Horizontal position is dependency depth: foundations at the left, endpoints at
the right. The deepest chain runs 56 modules.
click a node · 240 modules · 357 dependencies
Module
Nothing selected. Click a node, or
search above.
By area
Where the mass sits
Theorem counts are of named results in source. The audited figure
(1118) is larger because it counts every constant in the compiled environment,
including structure projections and instances.