Papers With

← All papers
First page of Formalization of Sullivan's No Wandering Domains Theorem in Lean

Formalization of Sullivan's No Wandering Domains Theorem in Lean

Ziang Li, Yusheng Luo

math.HO Sep 10, 2026 · v1
formalization autoformalization analysis
Read PDF arXiv abstract Code
TL;DR
Lean 4 formalization of Sullivan's No Wandering Domains theorem, building normal families, quasiconformal, and measurable Riemann mapping infrastructure on Mathlib.
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.
Problem

Sullivan's No Wandering Domains theorem states that every Fatou component of a rational self-map of the Riemann sphere of degree at least two is eventually periodic. Its proof requires extensive complex-analytic and dynamical infrastructure not previously available in Lean.

Approach

The theorem is decomposed into layers: normal families, Julia/Fatou sets, local Sobolev regularity, Wirtinger derivatives, Cauchy and Beurling transforms, quasiconformality, and the measurable Riemann mapping theorem. The formal proof follows McMullen's notes, constructing a space of invariant Beltrami differentials and solving the ∂̄-equation to derive a contradiction via a dimension count and density of repelling periodic points. Development used autoformalization with Claude Code on top of Mathlib, RMT4, and Carleson.

Results

The project comprises 171 Lean files and roughly 157,000 lines, with no uses of sorry, admit, or project-specific axioms. It formalizes Sullivan's theorem and, separately, the measurable Riemann mapping theorem, plus reusable analytic components like the Cauchy transform.