Papers With

← All papers
First page of Absence of bounded-orbit wandering domains

Absence of bounded-orbit wandering domains

Nikolai Prochorov, Lasse Rempe, James Waterman

math.DS Sep 23, 2026 · v1 math.CV
formalization autoformalization analysis
Read PDF arXiv abstract Code
TL;DR
The main proof was autoformalized in Lean 4 using generative AI, with the formal proofs released in a GitHub repository.
Abstract
We prove that transcendental entire functions do not have bounded-orbit wandering domains. This answers a long-standing open question. In fact, we prove a more general theorem, establishing the absence of certain wandering domains even for locally defined analytic functions. The proof is based on a recent remarkable argument of Ye, who obtained an elementary proof of Sullivan's classical theorem that rational maps do not have wandering domains.
Problem

Whether transcendental entire functions can have bounded-orbit wandering domains has been a long-standing open question in holomorphic dynamics.

Approach

The authors adapt Ye's elementary hyperbolic-area argument for Sullivan's no-wandering-domains theorem. The key ingredient is a uniform comparison of hyperbolic area estimates on compact sets, which handles the possibly infinite set of singular values. The argument is first carried out for locally defined analytic functions and then applied to entire functions. The proof was also autoformalized in Lean 4 with generative AI.

Results

Transcendental entire functions have no bounded-orbit wandering domains. A more general theorem rules out certain wandering domains for locally defined analytic functions. A Lean 4 formalization of the proof is publicly available.