PDElib is a Lean library of PDE and functional analysis,
and every result in it 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 main 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. (Hand-drawn; the explorer below is generated from the sources.)
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. In PDElib the deepest chain runs
58 modules.
click a node
Module
Nothing selected. Click a node, or
search above.
By area
Where the mass sits
Areas and counts for PDElib. Theorem counts are of named results in source;
the audited figure (1489) is larger because it counts every
constant in the compiled environment, including structure projections and instances.