# Formalization of Sullivan's No Wandering Domains Theorem in Lean

Preprint · Ziang Li, Yusheng Luo

- Archive id: arxiv:2609.16027
- Published: 2026-09-10
- arXiv: https://arxiv.org/abs/2609.16027
- Citations: 0
- Source URL: https://arxiv.org/abs/2609.16027
- PDF: https://arxiv.org/pdf/2609.16027
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

Topics: [AI for Mathematics & Formal Proof](https://space-kitty.com/topics/ai-mathematics)

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.