Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Barth and Schneider prove that for every sequence (Sn)n≥1(S_n)_{n\geq1} of sets of complex numbers, none of which has a finite limit point, there are positive integers knk_n and a transcendental entire function ff such that

f(kn)(z)=0for all z∈Sn and all n≥1.f^{(k_n)}(z)=0\quad\text{for all }z\in S_n\text{ and all }n\geq1.

This is the question of Problem 229 answered in the affirmative; the problem allows kn≥0k_n\geq0, and the theorem gives kn≥1k_n\geq1. The paper is not held in the library, so its construction is not compiled here; this page records the result as the site credits it.

Formalization. The statement file of the formal-conjectures project (FormalConjectures/ErdosProblems/229.lean) marks the problem solved and points, through its formal_proof attribute, at a Lean 4 file in Boris Alexeev's lean-proofs repository, linked above at its revision of 2026-03-31 and dated by its first posting on 2025-12-28. That file declares itself a formalization of a solution to Problem 229, names Barth and Schneider as the authors of the original proof, and says that a proof chosen by ChatGPT was auto-formalized by Aristotle (from Harmonic) against the formal-conjectures statement; so it is recorded here as a formalization of this claim rather than as an independent result. Its theorem erdos_229 asserts, for sets SnS_n with empty derived set, a transcendental entire function ff and for each n≥1n\geq1 an order kk with f(k)f^{(k)} vanishing on SnS_n; the file contains no sorry and no axiom command at the pinned commit. This project has not built the file or audited its statement against the problem, so it supplies no formalized evidence; the site's label PROVED (LEAN) refers to this development.

Acceptance. The paper is refereed: K. F. Barth and W. J. Schneider, On a problem of Erdős concerning the zeros of the derivatives of an entire function, Proc. Amer. Math. Soc. 32, no. 1 (March 1972), 229--232. The site's curator, Thomas F. Bloom, marks Problem 229 proved and credits this paper with the solution. The page is dated by the first day of the issue month. The publisher's record gives only the year 1972 and the issue, volume 32, number 1; March is that issue's month in the journal's 1972 schedule, and the paper's first posting carries no finer date.