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

8 declarations, 6 contain sorry, 0 declared as axioms

Erdős Problem 329: Maximum Density of Sidon Sets

References:

erdosproblems.com/329
[AlMi25] B. Alexeev and D. G. Mixon, Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof. arXiv:2510.19804 (2025).
[Ha47] Hall, Jr., Marshall, Cyclic projective planes. Duke Math. J. (1947), 1079--1090.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

def Erdos329.sqrtPartialDensity The partial density of a Sidon set A up to N, normalized by dividing by √N instead of N line 39 source
Source documentation
The partial density of a Sidon set A up to N, normalized by dividing by √N instead of N. This measures how close the set comes to the optimal density for Sidon sets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real
Proof uses: HDiv.hDiv, Set.ncard, Inter.inter, Set.Icc, OfNat.ofNat, Real.sqrt
8 instances, coercions and auxiliary constants left out.
```
noncomputable def sqrtPartialDensity (A : Set ℕ) (N : ℕ) : ℝ :=
…
```
def Erdos329.sidonUpperDensity The upper density of a Sidon set A, normalized by √N line 43 source
Source documentation
The upper density of a Sidon set A, normalized by √N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, Real
Proof uses: Filter.limsup, Erdos329.sqrtPartialDensity, Filter.atTop
3 instances, coercions and auxiliary constants left out.
```
noncomputable def sidonUpperDensity (A : Set ℕ) : ℝ :=
…
```
theorem Erdos329.erdos_329 Erdős Problem 329 sorry line 53 source
Source documentation
Erdős Problem 329. Let A ⊆ ℕ be a Sidon set. How large can lim sup_{N → ∞} |A ∩ {1,…,N}| / N^{1/2} be?

depends on sorry what this means
Statement uses: Eq, Real, SupSet.sSup, Set.ofPred, Exists, Set, Nat, IsSidon, Erdos329.sidonUpperDensity, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_329 : sSup {sidonUpperDensity A | (A : Set ℕ) (_ : IsSidon A)} =
    answer(sorry) := by
…
```
Mentions: Erdos329.sidonUpperDensity, IsSidon
theorem Erdos329.erdos_329.variants.lower_bound Erdős proved that upper density 1 / 2 can be attained; in particular, there exists a Sidon set whose upper density is at least 1 / 2 sorry line 62 source
Source documentation
Erdős proved that upper density 1 / 2 can be attained; in particular, there exists a Sidon set whose upper density is at least 1 / 2.

depends on sorry what this means
Statement uses: Exists, Set, Nat, And, IsSidon, GE.ge, Real, Erdos329.sidonUpperDensity, HDiv.hDiv, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_329.variants.lower_bound : ∃ (A : Set ℕ), IsSidon A ∧ sidonUpperDensity A ≥ 1/2 := by
…
```
Mentions: IsSidon, Erdos329.sidonUpperDensity
theorem Erdos329.erdos_329.variants.kruckeberg_1961 Krückeberg ([Kr61]) exhibited an infinite Sidon set A with sidonUpperDensity A = 1 / Real.sqrt 2, improving Erdős’ earlier 1 / 2 lower bound sorry line 73 source
Source documentation
Krückeberg ([Kr61]) exhibited an infinite Sidon set A with sidonUpperDensity A = 1 / Real.sqrt 2, improving Erdős’ earlier 1 / 2 lower bound.
[Kr61] Krückeberg, Fritz, $B\sb{2}$-Folgen und verwandte Zahlenfolgen. J. Reine Angew. Math. (1961), 53-60.

depends on sorry what this means
Statement uses: Exists, Set, Nat, And, IsSidon, Eq, Real, Erdos329.sidonUpperDensity, HDiv.hDiv, OfNat.ofNat, Real.sqrt
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_329.variants.kruckeberg_1961 : ∃ (A : Set ℕ), IsSidon A ∧
    sidonUpperDensity A = 1 / Real.sqrt 2 := by
…
```
Mentions: IsSidon, Erdos329.sidonUpperDensity
theorem Erdos329.erdos_329.variants.turan_1941 Erdős and Turán [ErTu41] proved the upper bound of 1 sorry line 83 source
Source documentation
Erdős and Turán [ErTu41] proved the upper bound of 1.
[ErTu41] Erdős, P. and Turán, P., On a problem of Sidon in additive number theory, and on some related problems. J. London Math. Soc. (1941), 212-215.

depends on sorry what this means
Statement uses: Set, Nat, IsSidon, LE.le, Real, Erdos329.sidonUpperDensity, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_329.variants.turan_1941 : ∀ (A : Set ℕ), IsSidon A → sidonUpperDensity A ≤ 1 := by
…
```
Mentions: IsSidon, Erdos329.sidonUpperDensity
theorem Erdos329.erdos_329.variants.converse_implication The converse: if the maximum density is 1, then any finite Sidon set can be embedded in a perfect difference set modulo $n > 0$ sorry line 97 source
Source documentation
The converse: if the maximum density is 1, then any finite Sidon set can be embedded in a perfect difference set modulo $n > 0$.
Since the consequent is false (due to the counterexamples in [Ha47] and [AlMi25]), this implication is logically equivalent to the statement that the maximum upper density of Sidon sets is NOT 1. Because the maximum upper density problem is still open, the truth value of this implication is also an open research problem.

depends on sorry what this means
Statement uses: Eq, Real, SupSet.sSup, Set.ofPred, Exists, Set, Nat, IsSidon, Erdos329.sidonUpperDensity, OfNat.ofNat, Finset, GT.gt, And, LE.le, IsPerfectDifferenceSet
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_329.variants.converse_implication :
    (sSup {sidonUpperDensity A | (A : Set ℕ) (_ : IsSidon A)} = 1) →
    (∀ (A : Finset ℕ), IsSidon (A : Set ℕ) → ∃ (D : Set ℕ) (n : ℕ) (_ : n > 0),
      ↑A ⊆ D ∧ IsPerfectDifferenceSet D n) := by
…
```
Mentions: Erdos329.sidonUpperDensity, IsSidon, IsPerfectDifferenceSet
theorem Erdos329.exists_sidon_pos_density It is possible to construct a Sidon set with positive density sorry line 109 source
Source documentation
It is possible to construct a Sidon set with positive density.

depends on sorry what this means
Statement uses: Exists, Set, Nat, And, IsSidon, LT.lt, Real, OfNat.ofNat, Erdos329.sidonUpperDensity
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem exists_sidon_pos_density : ∃ (A : Set ℕ), IsSidon A ∧ 0 < sidonUpperDensity A := by
…
```
Mentions: IsSidon, Erdos329.sidonUpperDensity