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 of sets of complex numbers, none of which has a finite limit point, there are positive integers and a transcendental entire function such that
This is the question of Problem 229 answered in the affirmative; the problem allows , and the theorem gives . 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 with empty derived set, a transcendental entire
function and for each an order with vanishing on
; 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.