FormalConjectures/ErdosProblems/315.lean
Explanation legend Lean4 Domain Explanation Language (L4DEL)
L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.
- L4DEL
- Lean4 Domain Explanation Language
Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1
3 declarations, 1 contain sorry, 0 declared as axioms
Erdős Problem 315
References:
- erdosproblems.com/315
- [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
- [Ka25] Y. Kamio, Asymptotic analysis of infinite decompositions of a unit fraction into unit fractions. arXiv:2503.02317 (2025).
- [LiTa25] Z. Li and Q. Tang, On a conjecture of Erdős and Graham about the Sylvester's sequence. arXiv:2503.12277 (2025).
Imports (1)
- def
Erdos315.uDocumented declaration: u line 42 sourceSource documentation
The sequence $u_1=1$, $u_{n+1}=u_n(u_n+1)$, indexed here so that
u iis $u_{i+1}$:u 0 = 1,u 1 = 2,u 2 = 6,u 3 = 42, … (sou i + 1is Sylvester's sequence $2, 3, 7, 43, \ldots$).no axioms what this means
Statement uses:
Nat2 instances, coercions and auxiliary constants left out.
def u : ℕ → ℕ | 0 => 1 | n + 1 => u n * (u n + 1) /-- The Vardi constant $c_0=\lim u_n^{1/2^n}=1.264085\cdots$. With the `0`-indexing of `u`, the $n$-th term $u_n^{1/2^n}$ of the defining sequence is `(u i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))` at `i = n - 1`. -/ - def
Erdos315.c₀The Vardi constant $c_0=\lim u_n^{1/2^n}=1.264085\cdots$ line 49 sourceSource documentation
The Vardi constant $c_0=\lim u_n^{1/2^n}=1.264085\cdots$. With the
0-indexing ofu, the $n$-th term $u_n^{1/2^n}$ of the defining sequence is(u i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))ati = n - 1.standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses:
RealProof uses:
Filter.limUnder,Nat,Filter.atTop,HPow.hPow, Erdos315.u,HDiv.hDiv,OfNat.ofNat,HAdd.hAdd23 instances, coercions and auxiliary constants left out.
noncomputable def c₀ : ℝ := limUnder atTop fun i => (u i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1)) …
Mentions: Erdos315.u
- theorem
Erdos315.erdos_315Documented declaration: erdos_315 sorry line 65 sourceSource documentation
Let $u_1=1$ and $u_{n+1}=u_n(u_n+1)$, so that $\sum_{k\geq 1}\frac{1}{u_k+1}$ and $u_k=\lfloor c_0^{2^k}+1\rfloor$ for $k\geq 1$, where $$c_0=\lim u_n^{1/2^n}=1.264085\cdots.$$ Let $a_1<a_2<\cdots $ be any other sequence with $\sum \frac{1}{a_k}=1$. Is it true that $$\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 $u_1=2$ and $u_{n+1}=u_n^2-u_n+1$ (Sylvester's sequence), which is the same sequence shifted by $1$; we use the phrasing above as more faithful to [ErGr80]. The constant $c_0$ is called the Vardi constant.
depends on sorry what this means
Statement uses:
Iff,True,Nat,LT.lt,OfNat.ofNat,StrictMono,Exists,Ne,HAdd.hAdd, Erdos315.u,Eq,Real,tsum,HDiv.hDiv,SummationFilter.unconditional,Filter.liminf,HPow.hPow,Filter.atTop, Erdos315.c₀Proof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous54 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem erdos_315 : answer(True) ↔ ∀ a : ℕ → ℕ, (∀ i, 0 < a i) → StrictMono a → (∃ i, a i ≠ u i + 1) → ∑' i, (1 : ℝ) / a i = 1 → atTop.liminf (fun i => (a i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))) < c₀ := by …Mentions: Erdos315.u, Erdos315.c₀