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

11 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 1

Reference: erdosproblems.com/1

Imports (1)

FormalConjecturesUtil

abbrev Erdos1.IsSumDistinctSet Sum-distinct sets line 38 source
Source documentation
A finite set of naturals $A$ is said to be a sum-distinct set for $N \in \mathbb{N}$ if $A\subseteq\{1, ..., N\}$ and the sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$
L4DEL explanation
A finite set of naturals up to N is sum-distinct when no two different subsets add up to the same total.
1. The set A must be contained in the interval from 1 to N.
2. The map sending each subset S of A (taken from A.powerset) to its sum must be injective.
Sources and attribution: Pinned Lean source (1646ca16afd6)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: And, LE.le, Finset.Icc, OfNat.ofNat, Function.Injective, Subtype, Membership.mem, Finset.powerset, Erdos1.IsSumDistinctSet.match_1, Finset.sum, id
9 instances, coercions and auxiliary constants left out.
```
abbrev IsSumDistinctSet (A : Finset ℕ) (N : ℕ) : Prop :=
…
```
theorem Erdos1.erdos_1 Erdos Problem 1: sum-distinct sets need N of order 2^n sorry line 53 source
L4DEL explanation
The statement says there is no constant C with N at least C * 2^n for every sum-distinct set of size n inside 1..N, and the file marks this as solved.
1. The attribute reads category research solved, and the docstring says the original conjecture N >> 2^n is false because a machine-checked disproof builds sets with N / 2^n tending to zero.
2. The formal statement is the negation of "there is C > 0 such that for all N and every sum-distinct A the inequality C * 2^|A| < N holds (for N not zero)".
3. In this repository the proof body is sorry; the attribute points to an external formal proof at the URL it cites.
Prerequisites: Erdos1.IsSumDistinctSet
Sources and attribution: Pinned Lean source (1646ca16afd6)
depends on sorry what this means
Statement uses: Not, Exists, Real, And, GT.gt, OfNat.ofNat, Nat, Finset, Erdos1.IsSumDistinctSet, Ne, LT.lt, HMul.hMul, HPow.hPow, Finset.card
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1 : ¬ ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℕ) (_ : IsSumDistinctSet A N),
    N ≠ 0 → C * 2 ^ A.card < N := by
…
```
Mentions: Erdos1.IsSumDistinctSet
theorem Erdos1.erdos_1.variants.weaker The trivial lower bound is $N \gg 2^n / n$ line 61 source
Source documentation
The trivial lower bound is $N \gg 2^n / n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Nat, Finset, Erdos1.IsSumDistinctSet, Ne, LT.lt, HDiv.hDiv, HMul.hMul, HPow.hPow, Finset.card
Proof uses: Exists.intro, And.intro, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool, Bool.true, LE.le, Finset.Icc, Function.Injective, Subtype and 121 more
176 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1.variants.weaker : ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℕ)
    (_ : IsSumDistinctSet A N), N ≠ 0 → C * 2 ^ A.card / A.card < N := by
…
```
Mentions: Erdos1.IsSumDistinctSet
theorem Erdos1.erdos_1.variants.lb Erdős and Moser [Er56] proved $$ N \geq (\tfrac{1}{4} - o(1)) \frac{2^n}{\sqrt{n}}. $$ [Er56] Erdős, P., Problems and results in additive number theory sorry line 90 source
Source documentation
Erdős and Moser [Er56] proved $$ N \geq (\tfrac{1}{4} - o(1)) \frac{2^n}{\sqrt{n}}. $$
[Er56] Erdős, P., Problems and results in additive number theory. Colloque sur la Th'{E}orie des Nombres, Bruxelles, 1955 (1956), 127-137.

depends on sorry what this means
Statement uses: Exists, Nat, Real, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Finset, Erdos1.IsSumDistinctSet, LE.le, HDiv.hDiv, HMul.hMul, HSub.hSub, Finset.card, HPow.hPow, Real.sqrt
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1.variants.lb : ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
    ∀ (N : ℕ) (A : Finset ℕ) (h : IsSumDistinctSet A N),
      (1 / 4 - o A.card) * 2 ^ A.card / (A.card : ℝ).sqrt ≤ N := by
…
```
Mentions: Erdos1.IsSumDistinctSet
theorem Erdos1.erdos_1.variants.lb_strong sorry line 102 source
depends on sorry what this means
Statement uses: Exists, Nat, Real, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Finset, Erdos1.IsSumDistinctSet, LE.le, HDiv.hDiv, HMul.hMul, HSub.hSub, Real.sqrt, Real.pi, Finset.card, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
abbrev Erdos1.IsSumDistinctRealSet A finite set of real numbers is said to be sum-distinct if all the subset sums differ by at least $1$ line 111 source
Source documentation
A finite set of real numbers is said to be sum-distinct if all the subset sums differ by at least $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Real, Nat
Proof uses: And, LE.le, Set, Set.Ioc, OfNat.ofNat, Set.Pairwise, Finset.powerset, Dist.dist, Finset.sum, id
14 instances, coercions and auxiliary constants left out.
```
abbrev IsSumDistinctRealSet (A : Finset ℝ) (N : ℕ) : Prop :=
…
```
theorem Erdos1.erdos_1.variants.real A generalisation of the problem to sets $A \subseteq (0, N]$ of real numbers, such that the subset sums all differ by at least $1$ is proposed in [Er73] and [ErGr80] line 127 source
Source documentation
A generalisation of the problem to sets $A \subseteq (0, N]$ of real numbers, such that the subset sums all differ by at least $1$ is proposed in [Er73] and [ErGr80].
The positive statement is false: every natural-number counterexample to erdos_1 embeds into $\mathbb{R}$, and distinct integer subset sums differ by at least one.
[Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

depends on sorry what this means
Statement uses: Not, Exists, Real, And, GT.gt, OfNat.ofNat, Nat, Finset, Erdos1.IsSumDistinctRealSet, Ne, LT.lt, HMul.hMul, HPow.hPow, Finset.card
Proof uses: Erdos1.erdos_1, Erdos1.IsSumDistinctSet, Exists.intro, And.intro, Function.Embedding, Function.Embedding.mk, Nat.cast_injective, Finset.map, LE.le, Set, Set.Ioc, Set.Pairwise, Finset.powerset, Dist.dist, Finset.sum, id, Membership.mem, Eq, Eq.mp, Finset.Icc and 86 more
133 instances, coercions and auxiliary constants left out.

Tactic trace: 107 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1.variants.real : ¬ ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℝ)
    (_ : IsSumDistinctRealSet A N), N ≠ 0 → C * 2 ^ A.card < N := by
…
```
Mentions: Erdos1.IsSumDistinctRealSet
theorem Erdos1.erdos_1.variants.least_N_3 The minimal value of $N$ such that there exists a sum-distinct set with three elements is $4$ line 228 source
Source documentation
The minimal value of $N$ such that there exists a sum-distinct set with three elements is $4$.
https://oeis.org/A276661

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, Finset, And, Erdos1.IsSumDistinctSet, Eq, Finset.card, OfNat.ofNat
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Exists.intro, Insert.insert, Singleton.singleton, Eq.mpr, id, Eq.trans, True, congrArg, congrFun', HAdd.hAdd, Finset.card_insert_of_notMem, of_eq_true, Not, False, Or, congr and 71 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1.variants.least_N_3 :
    IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3 } 4 := by
…
```
Mentions: Erdos1.IsSumDistinctSet
theorem Erdos1.erdos_1.variants.least_N_4 The minimal value of $N$ such that there exists a sum-distinct set with four elements is $7$ line 259 source
Source documentation
The minimal value of $N$ such that there exists a sum-distinct set with four elements is $7$.
https://oeis.org/A276661

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, Finset, And, Erdos1.IsSumDistinctSet, Eq, Finset.card, OfNat.ofNat
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Exists.intro, Insert.insert, Singleton.singleton, LE.le, Finset.Icc, Function.Injective, Subtype, Finset.powerset, Erdos1.IsSumDistinctSet.match_1, Finset.sum, id, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl and 10 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1.variants.least_N_4 :
    IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 4 } 7 := by
…
```
Mentions: Erdos1.IsSumDistinctSet
theorem Erdos1.erdos_1.variants.least_N_5 The minimal value of $N$ such that there exists a sum-distinct set with five elements is $13$ line 280 source
Source documentation
The minimal value of $N$ such that there exists a sum-distinct set with five elements is $13$.
https://oeis.org/A276661

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, Finset, And, Erdos1.IsSumDistinctSet, Eq, Finset.card, OfNat.ofNat
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Exists.intro, Insert.insert, Singleton.singleton, LE.le, Finset.Icc, Function.Injective, Subtype, Finset.powerset, Erdos1.IsSumDistinctSet.match_1, Finset.sum, id, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl and 10 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1.variants.least_N_5 :
    IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 5 } 13 := by
…
```
Mentions: Erdos1.IsSumDistinctSet
theorem Erdos1.erdos_1.variants.least_N_9 The minimal value of $N$ such that there exists a sum-distinct set with nine elements is $161$ sorry line 301 source
Source documentation
The minimal value of $N$ such that there exists a sum-distinct set with nine elements is $161$.
https://oeis.org/A276661

depends on sorry what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, Finset, And, Erdos1.IsSumDistinctSet, Eq, Finset.card, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1.variants.least_N_9 :
    IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 9 } 161 := by
…
```
Mentions: Erdos1.IsSumDistinctSet