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

4 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 288

Reference: erdosproblems.com/288

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

theorem Erdos288.erdos_288 Is it true that there are only finitely many pairs of intervals $I_1$, $I_2$ such that $$ \sum_{n_1 \in I_1} \frac{1}{n_1} + \sum_{n_2 \in I_2} \frac{1}{n_2} \in \mathbb{N}? $$ sorry line 37 source
Source documentation
Is it true that there are only finitely many pairs of intervals $I_1$, $I_2$ such that $$ \sum_{n_1 \in I_1} \frac{1}{n_1} + \sum_{n_2 \in I_2} \frac{1}{n_2} \in \mathbb{N}? $$

depends on sorry what this means
Statement uses: Iff, True, Set.Finite, Fin, OfNat.ofNat, Nat, Prod, PNat, Set.ofPred, And, LE.le, Prod.fst, Prod.snd, Exists, Eq, Rat, Finset.sum, Finset.univ, Set.toFinset, Set.Icc and 1 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_288 : answer(sorry) ↔ Set.Finite { I : Fin 2 → ℕ+ × ℕ+ |
    ∀ j, (I j).1 ≤ (I j).2 ∧
      ∃ n : ℕ+, (∑ j : Fin 2, ∑ nⱼ ∈ Set.Icc (I j).1 (I j).2, (nⱼ⁻¹ : ℚ)) = n } := by
…
```
theorem Erdos288.erdos_288.variants.i2_card_eq_1 This is still open even if $|I_2| = 1$ sorry line 46 source
Source documentation
This is still open even if $|I_2| = 1$.

depends on sorry what this means
Statement uses: Iff, True, Set.Finite, Prod, PNat, Set.ofPred, Erdos288.erdos_288.variants.i2_card_eq_1.match_1, And, LE.le, Prod.fst, Prod.snd, Exists, Eq, Rat, HAdd.hAdd, Finset.sum, Set.toFinset, Set.Icc, Inv.inv
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_288.variants.i2_card_eq_1 : answer(sorry) ↔ Set.Finite { (I, n₂) : (ℕ+ × ℕ+) × ℕ+ |
    I.1 ≤ I.2 ∧ ∃ n : ℕ+, ∑ n₁ ∈ Set.Icc I.1 I.2, (n₁⁻¹ : ℚ) + (n₂⁻¹ : ℚ) = n } := by
…
```
theorem Erdos288.erdos_288.variants.k_intervals It is perhaps true with two intervals replaced by any $k$ intervals sorry line 54 source
Source documentation
It is perhaps true with two intervals replaced by any $k$ intervals.

depends on sorry what this means
Statement uses: Iff, True, Nat, Set.Finite, Fin, Prod, PNat, Set.ofPred, And, LE.le, Prod.fst, Prod.snd, Exists, Eq, Rat, Finset.sum, Finset.univ, Set.toFinset, Set.Icc, Inv.inv
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_288.variants.k_intervals : answer(sorry) ↔ ∀ k, Set.Finite { I : Fin k → ℕ+ × ℕ+ |
    ∀ j, (I j).1 ≤ (I j).2 ∧
      ∃ n : ℕ+, (∑ j : Fin k, ∑ nⱼ ∈ Set.Icc (I j).1 (I j).2, (nⱼ⁻¹ : ℚ)) = n } := by
…
```
theorem Erdos288.erdos_288.variants.exists_k_gt_2 Is it true for any $k > 2$ that only finitely many $k$ intervals satisfy this condition? sorry line 63 source
Source documentation
Is it true for any $k > 2$ that only finitely many $k$ intervals satisfy this condition?

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, And, GT.gt, OfNat.ofNat, Set.Finite, Fin, Prod, PNat, Set.ofPred, LE.le, Prod.fst, Prod.snd, Eq, Rat, Finset.sum, Finset.univ, Set.toFinset and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_288.variants.exists_k_gt_2 : answer(sorry) ↔
    ∃ k > 2, Set.Finite { I : Fin k → ℕ+ × ℕ+ |
      ∀ j, (I j).1 ≤ (I j).2 ∧
        ∃ n : ℕ+, (∑ j : Fin k, ∑ nⱼ ∈ Set.Icc (I j).1 (I j).2, (nⱼ⁻¹ : ℚ)) = n } := by
…
```