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?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

315.lean

Retained formal statement1 of 1

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?

This is true, and was proved independently by Kamio [Ka25] and Li and Tang [LiTa25].

An earlier interpretation of this question on this site defined u1=2u_1=2 and un+1=un2un+1u_{n+1}=u_n^2-u_n+1 (Sylvester's sequence), which is the same sequence shifted by 11; we use the phrasing above as more faithful to [ErGr80]. The constant c0c_0 is called the Vardi constant.

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.

Search problems.science

Find a Problem, Result, source, or page