148.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

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

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

12 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 148

References:

erdosproblems.com/148
[ElPl21] Elsholtz, Christian and Planitzer, Stefan, Sums of four and more unit fractions and approximate parametrizations. Bull. Lond. Math. Soc. (2021), 695-709.
[Ko14] Konyagin, S. V., Double exponential lower bound for the number of representations of unity by Egyptian fractions. Math. Notes (2014), 277-281.
OEIS A006585

Imports (1)

FormalConjecturesUtil

def Erdos148.F Documented declaration: F line 41 source
Source documentation
F k is the number of solutions to $1 = \frac{1}{n_1} + \cdots + \frac{1}{n_k}$ with $1 \leq n_1 < \cdots < n_k$, that is, the number of $k$-element sets of positive integers whose reciprocals sum to $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Set.ncard, Finset, Set.ofPred, And, Eq, Finset.card, Not, Membership.mem, OfNat.ofNat, Rat, Finset.sum, HDiv.hDiv
9 instances, coercions and auxiliary constants left out.
```
noncomputable def F (k : ℕ) : ℕ :=
…
```
def Erdos148.u The sequence $u_0 = 1$, $u_{n+1} = u_n(u_n + 1)$ of [ElPl21, Corollary 3]: $1, 2, 6, 42, 1806, \ldots$, a shifted copy of Sylvester's sequence line 47 source
Source documentation
The sequence $u_0 = 1$, $u_{n+1} = u_n(u_n + 1)$ of [ElPl21, Corollary 3]: $1, 2, 6, 42, 1806, \ldots$, a shifted copy of Sylvester's sequence. This is the sequence Erdos315.u of Erdős Problem 315.

no axioms what this means
Statement uses: Nat
2 instances, coercions and auxiliary constants left out.
```
def u : ℕ → ℕ
  | 0 => 1
  | n + 1 => u n * (u n + 1)

/-- The constant $c_0 = \lim_{n \to \infty} u_n^{2^{-n}} = 1.5979102\ldots$ of
[ElPl21, Corollary 3]. The sequence $u_n^{2^{-n}}$ is increasing and bounded by $2$
[ElPl21, Remark 3], so the limit is its supremum. This constant is the square of the Vardi
constant $1.26408\ldots$, which is `Erdos315.c₀`. -/
```
Mentions: Erdos315.c₀
def Erdos148.c₀ The constant $c_0 = \lim_{n \to \infty} u_n^{2^{-n}} = 1.5979102\ldots$ of [ElPl21, Corollary 3] line 55 source
Source documentation
The constant $c_0 = \lim_{n \to \infty} u_n^{2^{-n}} = 1.5979102\ldots$ of [ElPl21, Corollary 3]. The sequence $u_n^{2^{-n}}$ is increasing and bounded by $2$ [ElPl21, Remark 3], so the limit is its supremum. This constant is the square of the Vardi constant $1.26408\ldots$, which is Erdos315.c₀.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: iSup, Nat, HPow.hPow, Erdos148.u, HDiv.hDiv, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.
```
noncomputable def c₀ : ℝ := ⨆ n : ℕ, (u n : ℝ) ^ ((1 : ℝ) / 2 ^ n)
…
```
Mentions: Erdos148.u
theorem Erdos148.F_one The only representation of $1$ as a single unit fraction is $1 = \frac{1}{1}$ line 59 source
Source documentation
The only representation of $1$ as a single unit fraction is $1 = \frac{1}{1}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos148.F, OfNat.ofNat
Proof uses: Set, Finset, Set.ofPred, And, Finset.card, Not, Membership.mem, Rat, Finset.sum, HDiv.hDiv, Singleton.singleton, Set.ext, Eq.mpr, Iff, Exists, id, congr, congrArg, congrFun', funext and 22 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem F_one : F 1 = 1 := by
…
```
Mentions: Erdos148.F
theorem Erdos148.F_two $1$ is not a sum of two distinct unit fractions line 74 source
Source documentation
$1$ is not a sum of two distinct unit fractions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos148.F, OfNat.ofNat
Proof uses: Set, Finset, Set.ofPred, And, Finset.card, Not, Membership.mem, Rat, Finset.sum, HDiv.hDiv, EmptyCollection.emptyCollection, Set.ext, Eq.mpr, Iff, id, Eq.trans, False, congrArg, iff_false, implies_congr and 106 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem F_two : F 2 = 0 := by
…
```
Mentions: Erdos148.F
lemma Erdos148.eq_two_three_six If $0 < x < y < z$ and $1 = \frac{1}{x} + \frac{1}{y} + \frac{1}{z}$, then $(x, y, z) = (2, 3, 6)$ line 97 source
Source documentation
If $0 < x < y < z$ and $1 = \frac{1}{x} + \frac{1}{y} + \frac{1}{z}$, then $(x, y, z) = (2, 3, 6)$.
```
private lemma eq_two_three_six {x y z : ℕ} (hx : 0 < x) (hxy : x < y) (hyz : y < z)
    (h : (1 : ℚ) / x + 1 / y + 1 / z = 1) : x = 2 ∧ y = 3 ∧ z = 6 := by
…
```
theorem Erdos148.F_three The only representation of $1$ as a sum of three distinct unit fractions is $1 = \frac{1}{2} + \frac{1}{3} + \frac{1}{6}$ line 121 source
Source documentation
The only representation of $1$ as a sum of three distinct unit fractions is $1 = \frac{1}{2} + \frac{1}{3} + \frac{1}{6}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos148.F, OfNat.ofNat
Proof uses: Set, Finset, Set.ofPred, And, Finset.card, Not, Membership.mem, Rat, Finset.sum, HDiv.hDiv, Singleton.singleton, Insert.insert, Set.ext, Eq.mpr, Iff, id, congrArg, Iff.intro, Exists, Ne and 102 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
```
theorem F_three : F 3 = 1 := by
…
```
Mentions: Erdos148.F
theorem Erdos148.F_first_values The values $F(1), \ldots, F(8)$ are $1, 0, 1, 6, 72, 2320, 245765, 151182379$ (OEIS A006585) sorry line 155 source
Source documentation
The values $F(1), \ldots, F(8)$ are $1, 0, 1, 6, 72, 2320, 245765, 151182379$ (OEIS A006585). $F(8)$ is due to John Dethridge (2004). It was recomputed independently in the erdosproblems.com forum.

L4DEL explanation
The values $F(1), \ldots, F(8)$ are $1, 0, 1, 6, 72, 2320, 245765, 151182379$ (OEIS A006585). $F(8)$ is due to John Dethridge (2004). It was recomputed independently in the erdosproblems.com forum.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: And, Eq, Nat, Erdos148.F, OfNat.ofNat
Proof uses: And.intro, Erdos148.F_one, Erdos148.F_two, Erdos148.F_three, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem F_first_values :
    F 1 = 1 ∧ F 2 = 0 ∧ F 3 = 1 ∧ F 4 = 6 ∧ F 5 = 72 ∧ F 6 = 2320 ∧ F 7 = 245765 ∧
      F 8 = 151182379 := by
…
```
Mentions: Erdos148.F
theorem Erdos148.u_first_values The first values of the sequence are $1, 2, 6, 42, 1806$ line 163 source
Source documentation
The first values of the sequence are $1, 2, 6, 42, 1806$.

no axioms what this means
Statement uses: And, Eq, Nat, Erdos148.u, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_first_values : u 0 = 1 ∧ u 1 = 2 ∧ u 2 = 6 ∧ u 3 = 42 ∧ u 4 = 1806 := by
…
```
Mentions: Erdos148.u
theorem Erdos148.erdos_148 Let $F(k)$ be the number of solutions to $$ 1= \frac{1}{n_1}+\cdots+\frac{1}{n_k},$$ where $1\leq n_1<\cdots<n_k$ are distinct integers sorry line 172 source
Source documentation
Let $F(k)$ be the number of solutions to $$ 1= \frac{1}{n_1}+\cdots+\frac{1}{n_k},$$ where $1\leq n_1<\cdots<n_k$ are distinct integers. Find good estimates for $F(k)$.

depends on sorry what this means
Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Erdos148.F, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_148 : (fun k ↦ (F k : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) := by
…
```
Mentions: Erdos148.F
theorem Erdos148.erdos_148.variants.lower_bound The current best bounds known are sorry line 189 source
Source documentation
The current best bounds known are $$2^{c^{\frac{k}{\log k}}}\leq F(k) \leq c_0^{(\frac{1}{5}+o(1))2^k},$$ where $c>0$ is some absolute constant and $c_0=1.5979102\ldots$ is the square of the 'Vardi constant' $1.26408\cdots$. The lower bound is due to Konyagin [Ko14] and the upper bound to Elsholtz and Planitzer [ElPl21]. (erdosproblems.com gives $c_0=1.26408\cdots$; [ElPl21, Remark 3] gives $c_0=1.5979102\ldots$.)
[Ko14, Theorem 1] states the lower bound in the explicit form $$F(k) \geq \exp\left(\exp\left(\left(\frac{(\log 2)(\log 3)}{3}+o(1)\right) \frac{k}{\log k}\right)\right) \quad (k \to \infty),$$ which is the statement formalised here.

depends on sorry what this means
Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, LE.le, Real.exp, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Real.log, Erdos148.F
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_148.variants.lower_bound :
    ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ᶠ k : ℕ in atTop,
      exp (exp ((log 2 * log 3 / 3 + o k) * ((k : ℝ) / log k))) ≤ F k := by
…
```
Mentions: Erdos148.F
theorem Erdos148.erdos_148.variants.upper_bound The current best bounds known are sorry line 207 source
Source documentation
The current best bounds known are $$2^{c^{\frac{k}{\log k}}}\leq F(k) \leq c_0^{(\frac{1}{5}+o(1))2^k},$$ where $c>0$ is some absolute constant and $c_0=1.5979102\ldots$ is the square of the 'Vardi constant' $1.26408\cdots$. The lower bound is due to Konyagin [Ko14] and the upper bound to Elsholtz and Planitzer [ElPl21]. (erdosproblems.com gives $c_0=1.26408\cdots$; [ElPl21, Remark 3] gives $c_0=1.5979102\ldots$.)
[ElPl21, Corollary 3(2)] shows that for every $\varepsilon > 0$ and all $k \geq k(\varepsilon)$, the number $f_k(1,1) \geq F(k)$ of solutions with $n_1 \leq \cdots \leq n_k$ is less than $c_0^{(\frac{2}{5}+\varepsilon)2^{k-1}} = c_0^{(\frac{1}{5}+\frac{\varepsilon}{2})2^k}$.

depends on sorry what this means
Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, LE.le, Erdos148.F, HPow.hPow, Erdos148.c₀, HMul.hMul, HAdd.hAdd, HDiv.hDiv
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_148.variants.upper_bound :
    ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ᶠ k : ℕ in atTop,
      (F k : ℝ) ≤ c₀ ^ ((1 / 5 + o k) * 2 ^ k) := by
…
```
Mentions: Erdos148.F, Erdos148.c₀