VOOZH about

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

⇱ Erdős Problem #229


👁 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
Previous
Next