Erdős Problem 1117: Maximum Modulus Points Distribution

### What is the conjecture

Let $f(z)$ be an entire function that is not a monomial. Define $\nu(r)$ as the number of points $z$ with $|z|=r$ where $|f(z)| = \max_{|z|=r}|f(z)|$ (which is finite for non-monomial entire functions).

**Question:** Can $\liminf_{r \to \infty} \nu(r) = \infty$?

**Status:** This is the second part of Erdős Problem 1117. The first part (whether $\limsup_{r \to \infty} \nu(r)=\infty$) was answered affirmatively by Herzog and Piranian. The second part remains open; Glücksam and Pardo-Simón have shown an "approximate" affirmative answer.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1117

### Prerequisites needed

**Formalizability Rating:** 2/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- Complex number absolute value and modulus properties
- Liminf and limsup of real-valued sequences
- Basic properties of entire functions (infinite differentiability, Taylor series)

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition and characterization of entire functions (analytic on all of ℂ)
- Definition of maximum modulus on circles and the counting function ν(r)

Rating justification (1-2 sentences): The statement relies on standard complex analysis definitions that have foundational support in Mathlib (complex numbers, topology, analysis). However, the specific definition of entire functions and properties of maximum modulus on circles will require some new definitions, though these are straightforward additions.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-30
* ams-32

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

Start by checking the available support for complex numbers, entire functions, maximum modulus on circles, liminf, and limsup. Formalize the conjecture's statement and counting function ν(r), using the linked source to resolve any subtle errors; done means the resulting Lean statement compiles.

Written by the indexing model from the issue text.