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

5 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 158

References:

erdosproblems.com/158
[ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.

Imports (1)

FormalConjecturesUtil

def Erdos158.B2 A set A ⊆ ℕ is said to be a B₂[g] set if for all n, the equation a + a' = n, a ≤ a', a, a' ∈ A has at most g solutions line 37 source
Source documentation
A set A ⊆ ℕ is said to be a B₂[g] set if for all n, the equation a + a' = n, a ≤ a', a, a' ∈ A has at most g solutions. This is defined in [ESS94].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set
Proof uses: LE.le, ENat, Set.encard, Prod, Set.ofPred, And, Eq, HAdd.hAdd, Prod.fst, Prod.snd, Membership.mem
7 instances, coercions and auxiliary constants left out.
```
def B2 (g : ℕ) (A : Set ℕ) : Prop :=
…
```
lemma Erdos158.b2_one A set is B₂[1] iff it is Sidon line 42 source
Source documentation
A set is B₂[1] iff it is Sidon.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Iff, Erdos158.B2, OfNat.ofNat, IsSidon
Proof uses: Iff.intro, Membership.mem, Eq, HAdd.hAdd, LE.le, Not, Or, And, Classical.em, Prod, Prod.mk, Iff.mp, ENat, Set.encard, Set.ofPred, Prod.fst, Prod.snd, Set.encard_le_one_iff, of_eq_true, Eq.trans and 12 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma b2_one {A : Set ℕ} : B2 1 A ↔ IsSidon A where
…
```
Mentions: Erdos158.B2, IsSidon
theorem Erdos158.erdos_158 Let A be an infinite B₂[2] set sorry line 60 source
Source documentation
Let A be an infinite B₂[2] set. Must liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0?

depends on sorry what this means
Statement uses: Iff, True, Set, Nat, Set.Infinite, Erdos158.B2, OfNat.ofNat, Eq, Real, Filter.liminf, HMul.hMul, Set.ncard, Inter.inter, Set.Iio, HPow.hPow, HDiv.hDiv, Neg.neg, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_158 : answer(sorry) ↔ ∀ A : Set ℕ, A.Infinite → B2 2 A →
    liminf (fun N : ℕ => (A ∩ .Iio N).ncard * (N : ℝ) ^ (- 1 / 2 : ℝ)) atTop = 0 := by
…
```
Mentions: Erdos158.B2
theorem Erdos158.erdos_158.variants.isSidon' Let A be an infinite Sidon set sorry line 67 source
Source documentation
Let A be an infinite Sidon set. Then liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) * (log N) ^ (1 / 2) < ∞. This is proved in [ESS94].

depends on sorry what this means
Statement uses: Set, Nat, Set.Infinite, IsSidon, LT.lt, ENNReal, Filter.liminf, ENNReal.ofReal, HMul.hMul, Real, Set.ncard, Inter.inter, Set.Iio, HPow.hPow, HDiv.hDiv, Neg.neg, OfNat.ofNat, Real.log, Filter.atTop, Top.top
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_158.variants.isSidon' {A : Set ℕ} (hAinf : A.Infinite) (hAsid : IsSidon A) :
    liminf (fun N ↦ ENNReal.ofReal ((A ∩ .Iio N).ncard * N ^ (- 1 / 2 : ℝ) * log N ^ (1 / 2 : ℝ)))
      atTop < ⊤ := by
…
```
Mentions: IsSidon
theorem Erdos158.erdos_158.variants.isSidon As a corollary of erdos_158.isSidon', we can prove that liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0 for any infinite Sidon set A line 75 source
Source documentation
As a corollary of erdos_158.isSidon', we can prove that liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0 for any infinite Sidon set A.

depends on sorry what this means
Statement uses: Set, Nat, Set.Infinite, IsSidon, Eq, Real, Filter.liminf, HMul.hMul, Set.ncard, Inter.inter, Set.Iio, HPow.hPow, HDiv.hDiv, Neg.neg, OfNat.ofNat, Filter.atTop
Proof uses: LT.lt, ENNReal, ENNReal.ofReal, Real.log, Top.top, Erdos158.erdos_158.variants.isSidon', Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, Ne, LE.le, id, implies_congr, Eq.refl, congrArg, Filter.Tendsto.liminf_eq, Filter.Tendsto.comp, nhds, ENNReal.tendsto_ofReal_atTop, And and 106 more
155 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_158.variants.isSidon {A : Set ℕ} (hAinf : A.Infinite) (hAsid : IsSidon A) :
    liminf (fun N : ℕ => (A ∩ .Iio N).ncard * (N : ℝ) ^ (- 1 / 2 : ℝ)) atTop = 0 := by
…
```
Mentions: IsSidon