156.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, 3 contain sorry, 0 declared as axioms

Erdős Problem 156

References:

erdosproblems.com/156
[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.
[Ru98b] Ruzsa, Imre Z., A small maximal Sidon set. Ramanujan J. (1998), 55-58.

Imports (1)

FormalConjecturesUtil

def Erdos156.minMaximalSidonSet The size of the smallest maximal Sidon set in $\{1, \dots, N\}$ line 39 source
Source documentation
The size of the smallest maximal Sidon set in $\{1, \dots, N\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Finset, Finset.image, Finset.card, Finset.filter, Set.IsMaximalSidonSetIn, Classical.propDecidable, Finset.powerset, Finset.Icc, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
noncomputable def minMaximalSidonSet (N : ℕ) : ℕ :=
…
```
theorem Erdos156.erdos_156 Does there exist a maximal Sidon set $A\subset \{1,\ldots,N\}$ of size $O(N^{1/3})$? sorry line 50 source
Source documentation
Does there exist a maximal Sidon set $A\subset \{1,\ldots,N\}$ of size $O(N^{1/3})$?
A question of Erdős, Sárközy, and Sós [ESS94].

depends on sorry what this means
Statement uses: Iff, True, Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos156.minMaximalSidonSet, HPow.hPow, HDiv.hDiv, OfNat.ofNat
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_156 :
    answer(sorry) ↔
      (fun N ↦ (minMaximalSidonSet N : ℝ)) =O[atTop] (fun N ↦ (N : ℝ) ^ (1 / 3 : ℝ)) := by
…
```
Mentions: Erdos156.minMaximalSidonSet
theorem Erdos156.greedySidonSet_isSidon line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, IsSidon, Finset, Finset.greedySidonBelow
Proof uses: Membership.mem, Set, Eq, HAdd.hAdd, LE.le, Prod.fst, Subtype, Finset.greedySidon.aux, Finset.filter_subset, Subtype.property
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Erdos156.erdos_156.variants.greedy_lower_bound It is easy to prove that the greedy construction of a maximal Sidon set in $\{1,\ldots,N\}$ has size $\gg N^{1/3}$ sorry line 66 source
Source documentation
It is easy to prove that the greedy construction of a maximal Sidon set in $\{1,\ldots,N\}$ has size $\gg N^{1/3}$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HPow.hPow, HDiv.hDiv, OfNat.ofNat, Finset.card, Finset.greedySidonBelow
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_156.variants.greedy_lower_bound :
    (fun N ↦ ((Finset.greedySidonBelow N).card : ℝ)) ≫ (fun N ↦ (N : ℝ) ^ (1 / 3 : ℝ)) := by
…
```
Mentions: Finset.greedySidonBelow
theorem Erdos156.erdos_156.variants.ruzsa_upper_bound Ruzsa [Ru98b] constructed a maximal Sidon set of size $\ll (N\log N)^{1/3}$ sorry line 74 source
Source documentation
Ruzsa [Ru98b] constructed a maximal Sidon set of size $\ll (N\log N)^{1/3}$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos156.minMaximalSidonSet, HPow.hPow, HMul.hMul, Real.log, HDiv.hDiv, OfNat.ofNat
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_156.variants.ruzsa_upper_bound :
    (fun N ↦ (minMaximalSidonSet N : ℝ)) ≪
      (fun N ↦ ((N : ℝ) * Real.log N) ^ (1 / 3 : ℝ)) := by
…
```
Mentions: Erdos156.minMaximalSidonSet