PreprintarXiv licencearXiv
Formalization of Sullivan's No Wandering Domains Theorem in Lean
Abstract
We report on a Lean 4 formalization of Sullivan's No Wandering Domains theorem: every Fatou component of a rational self-map of the Riemann sphere of degree at least two is eventually periodic. The project formalizes the relevant background in normal families, the Montel-Carathéodory theorem, Julia and Fatou sets, local Sobolev regularity and Wirtinger derivatives, the Cauchy and Beurling transforms, the equivalence of analytic and geometric quasiconformality, and the measurable Riemann mapping theorem. This paper describes the translation of this mathematics into Lean, the proof architecture, the reusable components, and the autoformalization workflow.
Related
- Global Regularity for the 3D Incompressible Navier–Stokes Equations via the Frohmanian Symplectic Tether: Lean 4 Formalization and Conditional Cubic Comparison Framework (v2.1)
- Formalization of Landau damping in the Vlasov--Poisson equations in Lean
- A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture
- A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture
- A Formalization of the Laplace Transform and Its Inversion in Lean 4
BibTeX
@misc{li2026formalization,
title = {{Formalization of Sullivan's No Wandering Domains Theorem in Lean}},
author = {Ziang Li and Yusheng Luo},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.16027},
eprint = {2609.16027},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.16027},
}
RIS
TY - UNPB
TI - Formalization of Sullivan's No Wandering Domains Theorem in Lean
AU - Ziang Li
AU - Yusheng Luo
PY - 2026
DA - 2026/09/10
PB - arXiv
DO - 10.48550/arxiv.2609.16027
UR - https://arxiv.org/abs/2609.16027
AB - We report on a Lean 4 formalization of Sullivan's No Wandering Domains theorem: every Fatou component of a rational self-map of the Riemann sphere of degree at least two is eventually periodic. The project formalizes the relevant background in normal families, the Montel-Carathéodory theorem, Julia and Fatou sets, local Sobolev regularity and Wirtinger derivatives, the Cauchy and Beurling transforms, the equivalence of analytic and geometric quasiconformality, and the measurable Riemann mapping theorem. This paper describes the translation of this mathematics into Lean, the proof architecture, the reusable components, and the autoformalization workflow.
ER -