Hironaka's resolution of singularities in characteristic zero
API documentation · Blueprint ·
Statements · formalization.yaml · Sources
A Lean 4 formalization, over Mathlib, of resolution of singularities in characteristic zero:
Hironaka's main theorems and their refinements by Kollár, Włodarczyk and Bierstone–Milman, for
algebraic schemes and for real- and complex-analytic manifolds and spaces. The main theorems are
listed below. The worked examples of the sources form a second library, HironakaExamples. Every
theorem is proved: neither library contains a sorry.
Main theorems
The main theorems are those named in comparator.json. Each is stated at the end
of the module that proves it, and again with sorry in a challenge file. A theorem from a source
names it in its docstring, in a paragraph Source statement: [Hir64, Main Theorem I, p. 132].
Verifying
The challenge files in Challenge/ state the main theorems with sorry proofs,
importing from this library only the Defs.lean files that define the vocabulary of the
statements. Read with those files, they say exactly what is claimed. Each also unfolds the
predicates its statements use, as examples. Challenge/Standard.lean
imports Mathlib only: it states the two definitions of the library that its first theorem uses,
with the library's names and bodies.
leanprover/comparator checks, for each name in
comparator.json, that the challenge statement and the library theorem are the
same and that the proof uses no axiom beyond propext, Classical.choice and Quot.sound. With
landrun and a lean4export built for this toolchain on the PATH:
lake build Hironaka Challenge
lake env path/to/comparator comparator.json # expect: Your solution is okay!
scripts/check_axioms.lean checks the same bound for every constant of
both libraries, so that none depends on sorryAx, and prints the axioms of each main theorem.
Building
The Lean toolchain is pinned in lean-toolchain and Mathlib in
lake-manifest.json. With elan installed, in the root of the repository:
lake exe cache get # fetch the prebuilt Mathlib
lake build # the library Hironaka
lake build HironakaExamples Challenge # examples, challenge files
scripts/ holds the checks run in CI: no axioms beyond the standard three, the
statement vocabulary in the Defs.lean files, the challenge files matching
comparator.json, the blueprint covering the statements, and others. Each is
described at the head of its file.
Layout
| path | contents |
|---|---|
Hironaka/ | the library, by role: the objects in Algebra/, Analytic/, Scheme/, Manifold/ and AnalyticSpace/, whose Defs.lean files hold what the statements use; the proof machinery in Resolution/, with the main theorems in folders named after the sources |
HironakaExamples/ | the worked examples and counterexamples of the sources; no module of Hironaka imports it |
Challenge.lean, Challenge/ | the main theorems stated against the definitions only |
comparator.json | the names of the main theorems, read by the comparator and the checks |
blueprint/ | the blueprint, a Verso document in a nested Lake package |
formalization.yaml | a machine-readable description of the project and of how each statement aligns with its source |
references.bib | the sources, under the keys by which everything cites them |
scripts/ | the checks, and the generators of the computed parts of formalization.yaml and of the blueprint's Sources list |
Documentation
The API documentation of Hironaka and HironakaExamples and the blueprint are linked at the top
of this file. The blueprint, in blueprint/, presents the statements to a
mathematical reader, with background chapters, a section for each main theorem and chapters on
the definitions the statements use.
formalization.yaml
formalization.yaml describes the project in the format of
mathlib-initiative/formalization.yaml
(version v0.4): the sources, the main results with their axioms, how the library was produced
and reviewed. Where the format leaves the shape open or has no field, this file adds:
alignment.statements: the format's suggested table, one entry per theorem matched with the item of the source it formalizes and its module, read from theSource statement:paragraphs of the docstrings; itsnotelists the labelled notes of the theorem's docstring (Gap, Correction, Interpretation, …), the same notes the blueprint shows.status.main_results[].statement_vocabulary: for each main result, the definition modules a reader needs to understand its statement.automation.methods[].cost.tokens: the model tokens of each phase of the work, beside the format's wall time and hardware.
The main results and the alignment table are generated from the library, so they stay current with it.
Sources
The sources, and the keys by which the docstrings and the blueprint cite them, are listed in the BibTeX file references.bib.
Provenance
This library was produced by an automated formalization process run by Claude Fable 5.1 (Anthropic),
directed and audited by Chris Elliott at Resolution, following the human-written sources listed in
the bibliography (references.bib), and then refactored and prepared for release
by Billy Snikkers and Adam Newgas at Resolution, also through Claude Code sessions. Every theorem is
checked by Lean's kernel; the axioms used are propext, Classical.choice and Quot.sound only.
License
Apache License 2.0; see LICENSE. Copyright (c) 2026 Resolution.