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.
The nine statements Lean assumes from the literature: each explained, with its citation and its literal Lean form.
Lean formalizations
The presentation has been formalized twice, in two separate Lean projects. Both started from the same source manuscript produced by GPT 5.5.
A Lean 4 formalization of the presentation theorem with no
sorry placeholders, built using Fable 5 and Opus 4.8. Lean treats
nine named mathematical results from the
literature as given, with a specific citation recorded for each. The
source is on
GitHub; its blueprint
and API documentation are linked above.
The repository carries a machine-readable
formalization.yaml
(in the community
format) recording the main statements, the axiom census, the
automation methods, and known divergences from the paper. Both main
results are also independently checkable with
leanprover/comparator
via the repository's
comparator-config.json,
whose Challenge.lean names one challenge theorem per main
result; step-by-step commands are on the
reproducibility page.
Note that this formalization is based on a version of Mathlib pinned at June 12, 2026, which does not include more recent progress on continuous cohomology.
An independent formalization using GPT 5.5 and Fable 5.
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.