Let $(S_n)_{n \ge 1}$ be a sequence of sets of complex numbers, none of which have a finite limit point. Does there exist an entire transcendental function $f(z)$ such that, for all $n \ge 1$, there exists some $k_n \ge 0$ such that $f^{(k_n)}(z) = 0$ for all $z \in S_n$.

Let $(S_n)_{n \ge 1}$ be a sequence of sets of complex numbers, none of which have a finite limit point. Does there exist an entire transcendental function $f(z)$ such that, for all $n \ge 1$, there exists some $k_n \ge 0$ such that $f^{(k_n)}(z) = 0$ for all $z \in S_n$.

This is Problem 2.30 in [Ha74], where it is attributed to Erdős.

Solved in the affirmative by Barth and Schneider [BaSc72].

This was formalized in Lean by Alexeev using Aristotle.