Fejér–Pólya conjecture: gap series with $n_k/k\to\infty$ assume every value infinitely often (Erdős #517)
Statement
Let $f(z)=\sum_{k=1}^\infty a_k z^{n_k}$ be a transcendental entire function written as a gap series: $n_1<n_2<\cdots$ are the exponents actually occurring, so $a_k\neq 0$ for all $k\geq 1$. Is it true that if $n_k/k\to\infty$ (the occurring exponents have density zero) then $f(z)$ assumes every complex value infinitely often?
Acceptance. FULLY RESOLVES: a complete proof that every gap series with $a_k\neq 0$ and $n_k/k\to\infty$ assumes every complex value infinitely often, OR an explicit counterexample — a gap series (exponents and coefficients given by explicit formulas) with $n_k/k\to\infty$ together with a proof that it omits some value or assumes some value only finitely often. Machine-checkable proof (Lean/Coq) preferred; else a full written proof with all steps. ADVANCES: a proof under hypotheses strictly weaker than the best partial results stated in the background (e.g. replacing $\sum 1/n_k<\infty$ by a weaker gap condition, or removing the finite-order assumption from the Pólya-type result); or a Lean formalization of one of the classical partial results [Fe08], [Bi28], [Po29] compiling against a current Mathlib. Deliver the proof file (or formalization repository with build instructions), or the counterexample construction with proof.
Background
A conjecture of Fejér and Pólya, recorded by Erdős [Er61, p.250]; listed as open on erdosproblems.com/517 (fetched 2026-07-13, status 'open', tagged 'analysis'). The known partial results run along two axes. Under the stronger gap condition $\sum 1/n_k<\infty$: Fejér [Fe08] proved $f$ assumes every value at least once, and Biernacki [Bi28] upgraded this to every value infinitely often. Under a growth restriction: Pólya [Po29] proved that if $f$ has finite order and $\limsup_k (n_{k+1}-n_k)=\infty$ then $f$ assumes every value infinitely often. The conjecture as stated — density-zero exponents ($n_k/k\to\infty$), no order restriction, no reciprocal-sum condition — remains open; it sits in classical value-distribution theory next to Picard's theorem (an entire function omits at most one value; the conjecture says gap series of this type omit none, and with infinite multiplicity). The site records the statement as already formalised. The attacker's tool: this is proof-shaped complex analysis (Wiman–Valiron / value-distribution methods for gap series); the concrete machine channel is Lean formalization of the Fejér, Biernacki, or Pólya partial results toward a formal frontier, since no finite computation can decide the conjecture itself.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #517 (T. F. Bloom) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.