Skip to content

Erdős problem 229

Let (Sn)n≥1(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)f(z) such that, for all n≥1n \ge 1, there exists some kn≥0k_n \ge 0 such that f(kn)(z)=0f^{(k_n)}(z) = 0 for all z∈Snz \in S_n.

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

229.lean

Retained formal statement1 of 2

Let (Sn)n≥1(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)f(z) such that, for all n≥1n \ge 1, there exists some kn≥0k_n \ge 0 such that f(kn)(z)=0f^{(k_n)}(z) = 0 for all z∈Snz \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.

FormalConjectures/ErdosProblems/229.leanErdos229.erdos_2294 linesExact file
True ↔  ∀ (S : ℕ → Set ℂ),    (∀ (n : ℕ), derivedSet (S n) = ∅) →      ∃ f, Transcendental (Polynomial ℂ) f ∧ Differentiable ℂ f ∧ ∀ n ≥ 1, ∃ k, ∀ z ∈ S n, iteratedDeriv k f z = 0
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page