VOOZH about

URL: https://www.erdosproblems.com/forum/thread/229

⇱ Erdős Problem #229 - Discussion thread

👁 Logo
Forum Inbox Favourites Tags
More
Forum
Dual View Random Solved Random Open
PROVED (LEAN) This has been solved in the affirmative and the proof verified in Lean.
Let $(S_n)_{n\geq 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\geq 1$, there exists some $k_n\geq 0$ such that\[f^{(k_n)}(z) = 0\textrm{ for all }z\in S_n?\]
#229: [Er57][Er61,p.250][Ha74][Er82e]
analysis | iterated functions
This is Problem 2.30 in [Ha74], where it is attributed to Erdős.

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

This problem has been formalised in Lean as part of the Google DeepMind Formal Conjectures project.

View the LaTeX source

This page was last edited 29 December 2025. View history

External data from the database - you can help update this
Formalised statement? Yes
1 comment on this problem
Likes this problem None
Interested in collaborating None
Currently working on this problem None
This problem looks difficult None
This problem looks tractable None
The results on this problem could be formalisable None
I am working on formalising the results on this problem None

Additional thanks to: AlphaProof and team, Zachary Chase, and Terence Tao

When referring to this problem, please use the original sources of Erdős. If you wish to acknowledge this website, the recommended citation format is:

T. F. Bloom, Erdős Problem #229, https://www.erdosproblems.com/229, accessed 2026-04-11
Order by oldest first or newest first. (The most recent comments are highlighted in a red border.)
All comments are the responsibility of the user. Comments appearing on this page are not verified for correctness. Please keep posts mathematical and on topic.

Log in to add a comment.

Back to the forum