Skip to content

Erdős problem 229

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/229.lean

Formal Conjectures

FormalConjectures/ErdosProblems/229.leanErdos229.erdos_2294 linesExact file
True  ∀ (S : ℕ → Set ℂ),    (∀ (n : ℕ), derivedSet (S n) = ∅) →f, Transcendental (Polynomial ℂ) fDifferentiablef ∧ ∀ n ≥ 1, ∃ k, ∀ zS 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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:229
  • PLBY Lean proofsErdosProblems.Erdos229

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Search problems.science

Find a Problem, Result, source, or page