Papers With

← All papers
First page of Cofinite Zeros of High Derivatives

Cofinite Zeros of High Derivatives

Eric Hou

math.CV Jul 23, 2026 · v1
formalization analysis
Read PDF arXiv abstract Code
TL;DR
A Lean 4 formalization (Mathlib v4.28.0) verifies the existence theorem, the explicit growth bound, and their supporting lemmas.
Abstract
We construct a nonzero transcendental entire function such that every nonempty open subset of the complex plane contains a zero of every sufficiently high derivative; equivalently, the union of the zero sets along every infinite increasing sequence of derivative orders is dense. The construction is probabilistic and uses a bounded-coefficient Fock series. A saddle estimate, a one-coordinate small-ball bound, and Jensen's formula give summable outer probabilities for zero-free disks. The resulting function satisfies the explicit growth bound $|f(z)|\leq\sqrt2\exp(|z|^2)$ and therefore also supplies a counterexample to a 1973 theorem of Boas and Reddy as printed. A machine-checked Lean 4 formalization verifies the existence theorem, the growth bound, and their supporting lemmas.
Problem

Erdős Problem #906 asks whether there is a transcendental entire function whose derivative zeros are eventually dense in every open set. A related 1973 Boas–Reddy theorem asserts the opposite for order-at-most-2 finite-type functions.

Approach

A nonzero transcendental entire function is constructed as a bounded-coefficient random Fock series with coefficients uniform on the unit disk. Saddle estimates, a one-coordinate small-ball bound, and Jensen's formula yield summable outer probabilities that derivatives have zero-free disks. A Borel–Cantelli-style argument over a countable base gives the cofinite conclusion. A Lean 4 formalization, pinned to Lean 4.28.0 and Mathlib v4.28.0, checks the existence theorem, the growth bound, and supporting lemmas with no sorry, admit, or custom axioms.

Results

Such a function exists satisfying |f(z)| ≤ √2·exp(|z|²), so every sufficiently high derivative has a zero in every nonempty open set, providing a counterexample to Boas–Reddy Theorem 1 as printed. The machine-checked Lean formalization confirms the main theorem and growth bound.