Skip to content

Erdős problem 315

Let u1=1u_1=1 and un+1=un(un+1)u_{n+1}=u_n(u_n+1), so that k11uk+1\sum_{k\geq 1}\frac{1}{u_k+1} and uk=c02k+1u_k=\lfloor c_0^{2^k}+1\rfloor for k1k\geq 1, where c0=limun1/2n=1.264085.c_0=\lim u_n^{1/2^n}=1.264085\cdots. Let a1<a2<a_1<a_2<\cdots be any other sequence with 1ak=1\sum \frac{1}{a_k}=1. Is it true that lim infan1/2n<c0=1.264085?\liminf a_n^{1/2^n}<c_0=1.264085\cdots?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/315.lean

Formal Conjectures

FormalConjectures/ErdosProblems/315.leanErdos315.erdos_3156 linesExact file
True  ∀ (a : ℕ → ℕ),    (∀ (i : ℕ), 0 < a i) →      StrictMono a        (∃ i, a iErdos315.u i + 1) →          ∑' (i : ℕ), 1 / ↑(a i) = 1 → Filter.liminf (fun i => ↑(a i) ^ (1 / 2) ^ (i + 1)) Filter.atTop < Erdos315.c
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:315
  • PLBY Lean proofsErdosProblems.Erdos315

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