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

19 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 304

Reference: erdosproblems.com/304

Imports (1)

FormalConjecturesUtil

def Erdos304.unitFractionExpressible The set of k for which a / b can be expressed as a sum of k distinct unit fractions line 34 source
Source documentation
The set of k for which a / b can be expressed as a sum of k distinct unit fractions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set
Proof uses: Set.ofPred, Exists, Finset, And, Eq, Finset.card, Membership.mem, GT.gt, OfNat.ofNat, Rat, HDiv.hDiv, Finset.sum, Inv.inv
10 instances, coercions and auxiliary constants left out.
```
def unitFractionExpressible (a b : ℕ) : Set ℕ :=
…
```
lemma Erdos304.zero_mem_unitFractionExpressible_iff line 38 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, Set, Erdos304.unitFractionExpressible, OfNat.ofNat, Or, Eq
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.ofPred, Exists, Finset, And, Finset.card, LT.lt, Rat, HDiv.hDiv, Finset.sum, Inv.inv, GT.gt, funext, forall_congr, implies_congr_ctx, Eq.refl and 7 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos304.unitFractionExpressible_of_zero line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Or, Eq, OfNat.ofNat, Set, Erdos304.unitFractionExpressible, Singleton.singleton
Proof uses: Eq.mpr, And, True, Membership.mem, id, Eq.trans, congrFun', congrArg, eq_true, Rat, HDiv.hDiv, congr, Finset, Finset.card, LT.lt, Finset.sum, Inv.inv, forall_congr, Set.ofPred, Exists and 80 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Erdos304.unitFractionExpressible_zero_left line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set, Erdos304.unitFractionExpressible, OfNat.ofNat, Singleton.singleton
Proof uses: Erdos304.unitFractionExpressible_of_zero, of_eq_true, Or, Eq.trans, True, congrFun', congrArg, eq_self, true_or
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos304.unitFractionExpressible_zero_right line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set, Erdos304.unitFractionExpressible, OfNat.ofNat, Singleton.singleton
Proof uses: Erdos304.unitFractionExpressible_of_zero, of_eq_true, Or, Eq.trans, True, congrArg, eq_self, or_true
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos304.zero_notMem_unitFractionExpressible line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Not, Membership.mem, Set, Erdos304.unitFractionExpressible, OfNat.ofNat, And, Ne
Proof uses: of_eq_true, Eq, Eq.trans, True, congrFun', congrArg, Or, Set.ofPred, Exists, Finset, Finset.card, LT.lt, Rat, HDiv.hDiv, Finset.sum, Inv.inv, GT.gt, funext, forall_congr, implies_congr_ctx and 8 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos304.eq_inv_of_one_mem_unitFractionExpressible line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Erdos304.unitFractionExpressible, OfNat.ofNat, Exists, And, LT.lt, Eq, Rat, HDiv.hDiv, Inv.inv
Proof uses: Finset, Singleton.singleton, Finset.sum, Eq.mp, Eq.trans, Set.ofPred, Finset.card, congrFun', congrArg, GT.gt, funext, forall_congr, implies_congr, Eq.refl, Exists.intro, And.intro, Finset.sum_singleton, Eq.symm
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Erdos304.dvd_of_one_mem_unitFractionExpressible line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, Erdos304.unitFractionExpressible, OfNat.ofNat, Dvd.dvd
Proof uses: And, LT.lt, Eq, Rat, HDiv.hDiv, Inv.inv, Exists, Erdos304.eq_inv_of_one_mem_unitFractionExpressible, Ne, False, Eq.mp, Eq.trans, congrFun', congrArg, CharP.cast_eq_zero, div_zero, Eq.symm, Exists.intro, HMul.hMul, cast and 48 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Erdos304.smallestCollection Documented declaration: smallestCollection line 92 source
Source documentation
Let $$N(a, b)$$, denoted here by smallestCollection a b be the minimal k such that there exist integers $1 < n_1 < n_2 < \dots < n_k$ with $$\frac{a}{b} = \sum_{i=1}^k \frac{1}{n_i}$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Erdos304.unitFractionExpressible
1 instances, coercions and auxiliary constants left out.
```
noncomputable def smallestCollection (a b : ℕ) : ℕ := sInf (unitFractionExpressible a b)
…
```
Mentions: Erdos304.unitFractionExpressible
lemma Erdos304.smallestCollection_pos in fact (unitFractionExpressible a b).Nonempty should always be true, but we do not prove it for now line 97 source
Source comment
in fact `(unitFractionExpressible a b).Nonempty` should always be true, but we do not prove it for now

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Set.Nonempty, Erdos304.unitFractionExpressible, LT.lt, Erdos304.smallestCollection
Proof uses: Eq, Membership.mem, Set, Eq.rec, Nat.sInf_mem, False.elim, False, Eq.mp, Eq.trans, Or, congr, congrArg, eq_false, id, Not, or_self, Decidable.byContradiction
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma smallestCollection_pos {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0)
    (h : (unitFractionExpressible a b).Nonempty) :
    0 < smallestCollection a b := by
…
```
Mentions: Erdos304.unitFractionExpressible, Erdos304.smallestCollection
lemma Erdos304.smallestCollection_left_one line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Erdos304.smallestCollection
Proof uses: Membership.mem, Set, Erdos304.unitFractionExpressible, Exists.intro, Finset, And, Finset.card, GT.gt, Rat, HDiv.hDiv, Finset.sum, Inv.inv, Singleton.singleton, Eq.mpr, id, Eq.trans, True, congr, congrArg, congrFun' and 19 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Erdos304.eq_one_of_smallestCollection_eq_one line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos304.smallestCollection, OfNat.ofNat, Exists, And, LT.lt, Rat, HDiv.hDiv, Inv.inv
Proof uses: Membership.mem, Set, Erdos304.unitFractionExpressible, Eq.rec, Nat.sInf_mem, Nat.nonempty_of_sInf_eq_succ, Erdos304.eq_inv_of_one_mem_unitFractionExpressible
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos304.dvd_of_smallestCollection_eq_one line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos304.smallestCollection, OfNat.ofNat, Dvd.dvd
Proof uses: Membership.mem, Set, Erdos304.unitFractionExpressible, Eq.rec, Nat.sInf_mem, Nat.nonempty_of_sInf_eq_succ, Erdos304.dvd_of_one_mem_unitFractionExpressible
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Erdos304.smallestCollection_two_fifteen line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Erdos304.smallestCollection, OfNat.ofNat
Proof uses: Membership.mem, Set, Erdos304.unitFractionExpressible, Exists.intro, Finset, And, Finset.card, GT.gt, Rat, HDiv.hDiv, Finset.sum, Inv.inv, Insert.insert, Singleton.singleton, of_eq_true, Eq.trans, True, congr, congrArg, congrFun' and 46 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def Erdos304.smallestCollectionTo Write $$N(b) = max_{1 \leq a < b} N(a, b)$$ line 139 source
Source documentation
Write $$N(b) = max_{1 \leq a < b} N(a, b)$$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, And, Membership.mem, Finset, Finset.Ico, OfNat.ofNat, Eq, Erdos304.smallestCollection
6 instances, coercions and auxiliary constants left out.
```
noncomputable def smallestCollectionTo (b : ℕ) : ℕ :=
…
```
theorem Erdos304.erdos_304.variants.upper_1950 In 1950, Erdős [Er50c] proved the upper bound $$N(b) \ll \log b / \log \log b$$ sorry line 147 source
Source documentation
In 1950, Erdős [Er50c] proved the upper bound $$N(b) \ll \log b / \log \log b$$. [Er50c] Erdős, P., Az ${1}/{x_1} + {1}/{x_2} + \ldots + {1}/{x_n} =A/B$ egyenlet eg'{E}sz sz'{A}m'{u} megold'{A}sairól. Mat. Lapok (1950), 192-210.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos304.smallestCollectionTo, HDiv.hDiv, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_304.variants.upper_1950 :
    (fun b => (smallestCollectionTo b : ℝ)) =O[atTop]
      (fun b => Real.log b / Real.log (Real.log b)) := by
…
```
Mentions: Erdos304.smallestCollectionTo
theorem Erdos304.erdos_304.variants.lower_1950 In 1950, Erdős [Er50c] proved the lower bound $$\log \log b \ll N(b)$$ sorry line 157 source
Source documentation
In 1950, Erdős [Er50c] proved the lower bound $$\log \log b \ll N(b)$$. [Er50c] Erdős, P., Az ${1}/{x_1} + {1}/{x_2} + \ldots + {1}/{x_n} =A/B$ egyenlet eg'{E}sz sz'{A}m'{u} megold'{A}sairól. Mat. Lapok (1950), 192-210.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Real.log, Erdos304.smallestCollectionTo
Proof uses: sorryAx, Lean.Name, Bool.false, 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_304.variants.lower_1950 :
    (fun b : ℕ => Real.log (Real.log b)) =O[atTop]
      (fun b => (smallestCollectionTo b : ℝ)) := by
…
```
Mentions: Erdos304.smallestCollectionTo
theorem Erdos304.erdos_304.variants.upper_1985 In 1985 Vose [Vo85] proved the upper bound $$N(b) \ll \sqrt{\log b}$$ sorry line 167 source
Source documentation
In 1985 Vose [Vo85] proved the upper bound $$N(b) \ll \sqrt{\log b}$$. [Vo85] Vose, Michael D., Egyptian fractions. Bull. London Math. Soc. (1985), 21-24.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos304.smallestCollectionTo, Real.sqrt, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, 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_304.variants.upper_1985 :
    (fun b => (smallestCollectionTo b : ℝ)) =O[atTop]
      (fun b => Real.sqrt (Real.log b)) := by
…
```
Mentions: Erdos304.smallestCollectionTo
theorem Erdos304.upper_bound Is it true that $$N(b) \ll \log \log b$$? sorry line 176 source
Source documentation
Is it true that $$N(b) \ll \log \log b$$?

depends on sorry what this means
Statement uses: Iff, True, Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos304.smallestCollectionTo, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, 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 upper_bound : answer(sorry) ↔
    (fun b : ℕ => (smallestCollectionTo b : ℝ)) =O[atTop] (fun b : ℕ => Real.log (Real.log b)) := by
…
```
Mentions: Erdos304.smallestCollectionTo