About these pages

These pages document the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). They were generated on 2026-09-03 by a script that reads the .lean files as text; no Lean was run to produce them. Consequences worth knowing:

• Statements are quoted textually from Theorems/Thm_….lean (the declaration up to := by p2m_exact_reverting …), with any leading licence header, the import lines and the generated attribute [-instance] … / attribute [-simp] … preamble removed and the remaining context lines (open, variable, universe, set_option, local notation) shown above the statement. They are not pretty-printed by Lean, so notation is exactly as the file spells it.
• Edges are imports. "T cites U" means the proof module P2M/Sol/S_T.lean has the line import Theorems.Thm_U. By the construction of the tree these are the theorems the proof uses, but an import is an upper bound on logical dependence: for 2,890 of the 106,853 citation edges (2.7%) the cited theorem's name does not occur textually in the importing proof (it may still be used through an instance or notation, or not at all); theorem pages mark those citations.
• "Below T" counts the distinct theorems in the import closure of T's proof module, as in the repository's documents. Depth is the length of a shortest citation path from fermat_last_theorem; 29,489 of the 29,511 theorems have one. The other 22 lie outside the citation closure of the final theorem: 19 are cited by no proof and are reached through a definition module that imports them (or a statement that mentions them), the remaining 3 only through those; their path says so.
• Proof sizes count the lines of the proof module after its import and preamble lines; helpers counts the theorem/lemma declarations in the proof module other than solution. Helpers are file-local and machine-named; they are not presented as library lemmas.
• Landmarks are the 49 theorems whose names occur in PROOF-PATH.md or in the route chapters. The step printed on other theorem pages ("under: …") is the step of the first landmark met going up one shortest path; it is a reading aid, not a classification.
• Identifier links inside statements are resolved textually against the declarations of the definition modules: an exact qualified name; a bare or partly qualified name completed through the statement's open lines or its own namespace; or field notation x.foo whose suffix names exactly one project constant in a visible namespace. An unlinked name is Mathlib's, a bound variable, or one the rule declined to guess.
• The Lean 4.33 port. 28 statement files were edited by hand when the tree was carried from Lean 4.30 to 4.33 and 52 import Def_Compat_Mathlib430; their pages carry a badge saying so. The 1,366 statements changed only by scripted token renames (e.g. ramificationIdx → ramificationIdx') are not badged.
• The English titles, informal statements, proof ideas and context paragraphs (on every theorem page and every definition-module page) are editorial additions kept outside the Lean files; the Lean statement on the same page is what is proved. Each such page carries the note English text generated automatically from the Lean source; the Lean statement is authoritative. The mathematics in that English text is typeset in your browser by a bundled copy of KaTeX; with scripts disabled, or if a formula does not parse, you see its TeX source instead. References are suggested automatically and have not been individually verified.
• Everything is proved: there are no conjectural or incomplete nodes, so the graphs use one colour. Boxes with a folded corner are definition modules.

Using the folder

Open html/index.html in a browser; no server is needed and nothing is fetched from the network. All links are relative. The links to .lean source files assume the folder sits at the root of the repository (next to Theorems/, P2M/, Definitions/); everything else works wherever the folder is. The interactive neighbourhood graphs use Graphviz compiled to WebAssembly (bundled); if a browser refuses to run it from a local file, the page says so and the lists carry the same information. Tested with a Chromium-based browser; the pages use only long-standing web features (classic scripts, SVG, no modules or network requests) so that Firefox and Safari behave the same from disk.

Third-party material

Graph layout: Graphviz via @hpcc-js/wasm (Apache-2.0). Mathematics typesetting: KaTeX (MIT; fonts SIL OFL 1.1). Licence texts are in assets/vendor/. The Lean files' own attribution is in ATTRIBUTION.md.