Explore the proof
Every statement paired with its Lean counterpart, with an interactive dependency graph; completion status is computed directly from the Lean code.
doc-gen4 pages for every declaration in the formalization; dependency links resolve to the public Mathlib docs.
Lean formalizations
The presentation has been formalized twice, in two separate Lean projects.
An end-to-end Lean proof of the presentation theorem with no
sorry placeholders. Lean treats nine named mathematical
results from the literature as given, with a specific citation recorded
for each.
A second Lean proof, begun independently and preserved in two stages.
Contains no sorry placeholders and uses no Lean code
from Roe's project. Lean treats six published results and four
project-specific steps as given; the release lists all ten.
On this site: blueprint ·
API documentation.
Proves four remaining steps using a documented adaptation from Roe's formalization. Its seven remaining external mathematical inputs are each tied to published literature.