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 ∑k≥11uk+1\sum_{k\geq 1}\frac{1}{u_k+1} and uk=⌊c02k+1⌋u_k=\lfloor c_0^{2^k}+1\rfloor for k≥1k\geq 1, where c0=lim⁡un1/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 inf⁡an1/2n<c0=1.264085⋯?\liminf a_n^{1/2^n}<c_0=1.264085\cdots?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

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 ∑k≥11uk+1\sum_{k\geq 1}\frac{1}{u_k+1} and uk=⌊c02k+1⌋u_k=\lfloor c_0^{2^k}+1\rfloor for k≥1k\geq 1, where c0=lim⁡un1/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 inf⁡an1/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=un2−un+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 i ≠ Erdos315.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.