---

Claim. Let $\mathfrak n<\mathfrak m<\mathfrak c$ be cardinals. A family of analytic functions taking at most $\mathfrak n$ distinct values at every point has at most $\mathfrak n$ members. This is the remark after the theorem in P. Erdős, An interpolation problem associated with the continuum hypothesis, Michigan Math. J. 11 (1964), 9--10 (p. 10), proved by the theorem's counting argument. Two distinct entire functions agree on a countable set, so in a subfamily of $\mathfrak n^+\le\mathfrak m$ functions fewer than $\mathfrak c$ points carry a coincidence, and at any other point the subfamily takes $\mathfrak n^+$ distinct values. For Problem 1119, with the problem's $\mathfrak m$ in the role of $\mathfrak n$, the answer is yes in ZFC for every $\mathfrak m>\aleph_0$ with $\mathfrak m^+<\mathfrak c$.

Covers. Every cardinal $\mathfrak m$ of the problem with $\mathfrak m^+<\mathfrak c$. The remaining case $\mathfrak m^+=\mathfrak c$ is undecidable by Kumar and Shelah's model and Schilhan and Weinert's result. Hayman's 1974 list calls the case $\mathfrak m^+<\mathfrak c$ easy to see, which is how the site's commentary records it.

Depends on. No page of this wiki.

Acceptance. Refereed: the result appears in a journal paper in the Michigan Mathematical Journal.

Formalization. The formalization link is Boris Alexeev's lean-proofs file src/latest/ErdosProblems/Erdos1119.lean, at the revision that formal-conjectures names as the formal proof of erdos_1119.variants.easy_case. Its header calls it a formalization of a solution to the problem and names Paul Erdős as the informal author and Codex and GPT-5.6 Sol as the formal authors. It proves erdos_1119.variants.easy_case and Erdős's countable theorem. The corpus has not built it, so no formalized evidence is listed. A separate Lean package by Collin Yuanjie Ren, noted in the community database, formalizes Erdős's countable-values theorem in both directions. The problem asks only about $\mathfrak m>\aleph_0$, so that package is not a claim about it.