Hironaka

Hironaka's resolution of singularities in characteristic zero, formalized in Lean 4 over Mathlib: the library Hironaka and the worked examples HironakaExamples. Every theorem is proved; neither library contains a sorry.

Source

The repository on GitHub.

 Blueprint

One section per main theorem, explaining the statement and its source, and chapters on the definitions the statements use, each embedding its declarations from the library.

 API documentation

Generated from library code and comments.