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

20 declarations, 12 contain sorry, 0 declared as axioms

Ben Green's Open Problem 31

Write $F(N)$ for the largest Sidon subset of $[N]$. Improve, at least for infinitely many $N$, the bounds $N^{1/2} + O(1) \le F(N) \le N^{1/2} + N^{1/4} + O(1)$.

Note: the upper bound was improved to $N^{1/2} + 0.98183 N^{1/4} + O(1)$ in [CHO25], and then to $N^{1/2} + 0.94349\ldots N^{1/4} + O(1)$ in [HZ26].

Related to Erdős Problem 30.

References:

[Gr24] [Ben Green's Open Problem 31](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.7 Problem 31)
[Gr01] Green, Ben. "The number of squares and $ B_h [g] $ sets." Acta Arithmetica 100.4 (2001): 365-390.
[BFR23] Balogh, József, Zoltán Füredi, and Souktik Roy. "An upper bound on the size of Sidon sets." The American Mathematical Monthly 130.5 (2023): 437-445.
[CHO25] Carter, Daniel, Zach Hunter, and Kevin O’Bryant. "On the diameter of finite Sidon sets." Acta Mathematica Hungarica 175.1 (2025): 108-126.
[HZ26] Hou, Jianfeng, and Hongbin Zhao. "An Improved Upper Bound for Finite Sidon Sets via Vector-Valued Smoothing." arXiv:2607.01169 (2026).
[ET41] Erdos, Paul, and Pál Turán. "On a problem of Sidon in additive number theory, and on some related problems." J. London Math. Soc 16.4 (1941): 212-215.
[Li69] Lindström, Bernt. “A remark on B4-Sequences.” Journal of Combinatorial Theory, Series A 7 (1969): 276-277.
[CLZ01] Cohen, G.D., Litsyn, S., & Zémor, G. (2001). Binary B2-Sequences : A New Upper Bound. J. Comb. Theory A, 94, 152-155.
[BS85] Babai, László, and Vera T. Sós. "Sidon sets in groups and induced subgraphs of Cayley graphs." European Journal of Combinatorics 6.2 (1985): 101-114. doi:10.1016/S0195-6698(85)80001-9

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

def Green31.F Let $F(N)$ be the largest Sidon subset of $[N]$ line 59 source
Source documentation
Let $F(N)$ be the largest Sidon subset of $[N]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Finset.maxSidonSubsetCard, Finset.Icc, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
noncomputable def F (N : ℕ) : ℝ := Finset.maxSidonSubsetCard (Finset.Icc 1 N)
…
```
Mentions: Finset.maxSidonSubsetCard
theorem Green31.green_31.lower Can we improve the lower bound $N^{1/2} + O(1)$, at least for infinitely many $N$? sorry line 63 source
Source documentation
Can we improve the lower bound $N^{1/2} + O(1)$, at least for infinitely many $N$?

depends on sorry what this means
Statement uses: Nat, Real, sorryAx, Bool.false, And, Filter.Tendsto, HSub.hSub, Real.sqrt, Filter.atTop, Filter.Frequently, LE.le, Green31.F
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_31.lower :
    let ans := (answer(sorry) : ℕ → ℝ)
…
```
theorem Green31.green_31.variants.lower_eventually Can we improve the lower bound $N^{1/2} + O(1)$, for all sufficiently large $N$? sorry line 71 source
Source documentation
Can we improve the lower bound $N^{1/2} + O(1)$, for all sufficiently large $N$?

depends on sorry what this means
Statement uses: Nat, Real, sorryAx, Bool.false, And, Filter.Tendsto, HSub.hSub, Real.sqrt, Filter.atTop, Filter.Eventually, LE.le, Green31.F
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_31.variants.lower_eventually :
    let ans := (answer(sorry) : ℕ → ℝ)
…
```
theorem Green31.green_31.upper Can we improve the upper bound $N^{1/2} + 0.94349 N^{1/4} + O(1)$ [HZ26], at least for infinitely many $N$? sorry line 82 source
Source documentation
Can we improve the upper bound $N^{1/2} + 0.94349 N^{1/4} + O(1)$ [HZ26], at least for infinitely many $N$?

depends on sorry what this means
Statement uses: Nat, Real, sorryAx, Bool.false, And, Filter.Frequently, LE.le, Green31.F, Filter.atTop, Exists, LT.lt, OfScientific.ofScientific, Bool.true, Filter.Eventually, HSub.hSub, Real.sqrt, HAdd.hAdd, HMul.hMul, HPow.hPow, Inv.inv and 1 more
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_31.upper :
    let ans := (answer(sorry) : ℕ → ℝ)
…
```
theorem Green31.green_31.variants.upper_eventually Can we improve the upper bound $N^{1/2} + 0.94349 N^{1/4} + O(1)$ [HZ26], for all sufficiently large $N$? sorry line 93 source
Source documentation
Can we improve the upper bound $N^{1/2} + 0.94349 N^{1/4} + O(1)$ [HZ26], for all sufficiently large $N$?

depends on sorry what this means
Statement uses: Nat, Real, sorryAx, Bool.false, And, Filter.Eventually, LE.le, Green31.F, Filter.atTop, Exists, LT.lt, OfScientific.ofScientific, Bool.true, HSub.hSub, Real.sqrt, HAdd.hAdd, HMul.hMul, HPow.hPow, Inv.inv, OfNat.ofNat
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_31.variants.upper_eventually :
    let ans := (answer(sorry) : ℕ → ℝ)
…
```
theorem Green31.green_31.variants.upper_li69 [Li69] proved $F(n) \le n^{1/2} + n^{1/4} + O(1)$ sorry line 101 source
Source documentation
[Li69] proved $F(n) \le n^{1/2} + n^{1/4} + O(1)$.

depends on sorry what this means
Statement uses: Exists, Real, Filter.Eventually, Nat, LE.le, Green31.F, HAdd.hAdd, Real.sqrt, HPow.hPow, Inv.inv, OfNat.ofNat, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_31.variants.upper_li69 :
    ∃ C : ℝ, ∀ᶠ N in atTop, F N ≤ Real.sqrt (N : ℝ) + (N : ℝ) ^ (4⁻¹ : ℝ) + C := by
…
```
Mentions: Green31.F
theorem Green31.green_31.variants.upper_bfr23 [BFR23] obtained a small improvement, getting an upper bound of $F(N) \le N^{1/2} + 0.998 N^{1/4}$ for large $N$ sorry line 110 source
Source documentation
[BFR23] obtained a small improvement, getting an upper bound of $F(N) \le N^{1/2} + 0.998 N^{1/4}$ for large $N$.

depends on sorry what this means
Statement uses: Filter.Eventually, Nat, LE.le, Real, Green31.F, HAdd.hAdd, Real.sqrt, HMul.hMul, OfScientific.ofScientific, Bool.true, HPow.hPow, Inv.inv, OfNat.ofNat, Filter.atTop
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 green_31.variants.upper_bfr23 :
    ∀ᶠ N in atTop, F N ≤ Real.sqrt (N : ℝ) + (0.998 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ) := by
…
```
Mentions: Green31.F
theorem Green31.green_31.variants.upper_cho25 The upper bound was further improved to $N^{1/2} + 0.98183 N^{1/4} + O(1)$ [CHO25] sorry line 116 source
Source documentation
The upper bound was further improved to $N^{1/2} + 0.98183 N^{1/4} + O(1)$ [CHO25].

depends on sorry what this means
Statement uses: Exists, Real, Filter.Eventually, Nat, LE.le, Green31.F, HAdd.hAdd, Real.sqrt, HMul.hMul, OfScientific.ofScientific, Bool.true, HPow.hPow, Inv.inv, OfNat.ofNat, Filter.atTop
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 green_31.variants.upper_cho25 :
    ∃ C : ℝ, ∀ᶠ N in atTop, F N ≤ Real.sqrt (N : ℝ) + (0.98183 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ) + C := by
…
```
Mentions: Green31.F
theorem Green31.green_31.variants.upper_hz26 [HZ26] improved the upper bound to $N^{1/2} + \gamma_0 N^{1/4} + O(1)$ with $\gamma_0 = 0.94349\ldots < 0.9435$ sorry line 125 source
Source documentation
[HZ26] improved the upper bound to $N^{1/2} + \gamma_0 N^{1/4} + O(1)$ with $\gamma_0 = 0.94349\ldots < 0.9435$.

depends on sorry what this means
Statement uses: Exists, Real, Filter.Eventually, Nat, LE.le, Green31.F, HAdd.hAdd, Real.sqrt, HMul.hMul, OfScientific.ofScientific, Bool.true, HPow.hPow, Inv.inv, OfNat.ofNat, Filter.atTop
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 green_31.variants.upper_hz26 :
    ∃ C : ℝ, ∀ᶠ N in atTop, F N ≤ Real.sqrt (N : ℝ) + (0.9435 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ) + C := by
…
```
Mentions: Green31.F
theorem Green31.green_31.variants.zmod_p It is not known whether or not there exists a Sidon subset of $\mathbb{Z}/p\mathbb{Z}$ of size $(1 + o(1))\sqrt{p}$, for all $p$ [Gr24] sorry line 134 source
Source documentation
It is not known whether or not there exists a Sidon subset of $\mathbb{Z}/p\mathbb{Z}$ of size $(1 + o(1))\sqrt{p}$, for all $p$ [Gr24].

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Finset, ZMod, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Nat.Prime, IsSidon, Eq, Finset.card, HMul.hMul, HAdd.hAdd, Real.sqrt
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_31.variants.zmod_p : answer(sorry) ↔
    ∃ S : (n : ℕ) → Finset (ZMod n),
    ∃ o : ℕ → ℝ,
      (o =o[atTop] fun _ : ℕ ↦ (1 : ℝ)) ∧
      (∀ p, p.Prime → IsSidon (S p : Set (ZMod p))) ∧
      (∀ p, p.Prime → ((S p).card : ℝ) = (1 + o p) * Real.sqrt (p : ℝ)) := by
…
```
Mentions: IsSidon
def Green31.IsGroupSidon A subset $S$ of an abelian group is a Sidon set of the first kind in the sense of Babai and Sós [BS85] if $a + b = c + d$ with $a, b, c, d \in S$ implies $|\{a, b, c, d\}| \le 2$ line 148 source
Source documentation
A subset $S$ of an abelian group is a Sidon set of the first kind in the sense of Babai and Sós [BS85] if $a + b = c + d$ with $a, b, c, d \in S$ implies $|\{a, b, c, d\}| \le 2$.
Unlike IsSidon, this allows $a + a = b + b$ with $a \ne b$.

no axioms what this means
Statement uses: AddCommGroup, Set
Proof uses: Membership.mem, Eq, HAdd.hAdd, Or, And
6 instances, coercions and auxiliary constants left out.
```
def IsGroupSidon {G : Type*} [AddCommGroup G] (S : Set G) : Prop :=
…
```
theorem Green31.isGroupSidon_of_isSidon line 153 source
no axioms what this means
Statement uses: AddCommGroup, Set, IsSidon, Green31.IsGroupSidon
Proof uses: Membership.mem, Eq, HAdd.hAdd, And, Or, Or.inl, Or.inr
8 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Green31.isGroupSidon_iff_isSidon The two notions agree in a group where $2a = 2b$ implies $a = b$, such as a group of odd order line 164 source
Source documentation
The two notions agree in a group where $2a = 2b$ implies $a = b$, such as a group of odd order.

no axioms what this means
Statement uses: AddCommGroup, Function.Injective, HAdd.hAdd, Set, Iff, Green31.IsGroupSidon, IsSidon
Proof uses: Iff.intro, Membership.mem, Eq, And, Or, Or.inl, Or.inr, And.intro, Green31.isGroupSidon_of_isSidon
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem isGroupSidon_iff_isSidon {G : Type*} [AddCommGroup G]
    (hG : Function.Injective fun a : G ↦ a + a) {S : Set G} : IsGroupSidon S ↔ IsSidon S := by
…
```
Mentions: Green31.IsGroupSidon, IsSidon
theorem Green31.subsingleton_of_isSidon_of_exponent_two In a group of exponent $2$ an IsSidon set has at most one element line 174 source
Source documentation
In a group of exponent $2$ an IsSidon set has at most one element.

standard axioms: propext what this means
Statement uses: AddCommGroup, Eq, HAdd.hAdd, OfNat.ofNat, Set, IsSidon, Set.Subsingleton
Proof uses: Membership.mem, And, Or, Eq.mpr, id, congrArg, Eq.refl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem subsingleton_of_isSidon_of_exponent_two {G : Type*} [AddCommGroup G]
    (hG : ∀ a : G, a + a = 0) {S : Set G} (hS : IsSidon S) : S.Subsingleton := by
…
```
Mentions: IsSidon
theorem Green31.isGroupSidon_klein Three points of the Klein four-group form a Sidon set in the sense of Babai and Sós line 181 source
Source documentation
Three points of the Klein four-group form a Sidon set in the sense of Babai and Sós.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Green31.IsGroupSidon, Prod, ZMod, OfNat.ofNat, Nat, Insert.insert, Set, Prod.mk, Singleton.singleton
Proof uses: Membership.mem, Eq, HAdd.hAdd, Or, And, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm
51 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem isGroupSidon_klein :
    IsGroupSidon ({(0, 0), (1, 0), (0, 1)} : Set (ZMod 2 × ZMod 2)) := by
…
```
Mentions: Green31.IsGroupSidon
theorem Green31.not_isGroupSidon_klein_univ The whole Klein four-group is not a Sidon set in the sense of Babai and Sós, since $(0, 0) + (1, 1) = (1, 0) + (0, 1)$ line 190 source
Source documentation
The whole Klein four-group is not a Sidon set in the sense of Babai and Sós, since $(0, 0) + (1, 1) = (1, 0) + (0, 1)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Green31.IsGroupSidon, Prod, ZMod, OfNat.ofNat, Nat, Set.univ
Proof uses: absurd, Or, And, Eq, Prod.mk, False, trivial, of_decide_eq_true, HAdd.hAdd, id, Bool, Decidable.decide, Bool.true, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem not_isGroupSidon_klein_univ : ¬ IsGroupSidon (Set.univ : Set (ZMod 2 × ZMod 2)) :=
…
```
Mentions: Green31.IsGroupSidon
theorem Green31.green_31.variants.abelian It is not known whether, if $G$ is an abelian group of size $n$, there always exists a Sidon subset of $G$ of size $0.01\sqrt{n}$ [Gr24] sorry line 204 source
Source documentation
It is not known whether, if $G$ is an abelian group of size $n$, there always exists a Sidon subset of $G$ of size $0.01\sqrt{n}$ [Gr24].
Green defines a Sidon set by $r_A(n) \le 1$ [Gr24, Section 4]. Read literally, this forbids $a + a = b + b$ with $a \ne b$, and the answer is trivially negative: a Sidon subset of a group of exponent $2$ then has at most one element. We use the definition of Babai and Sós [BS85] instead, see IsGroupSidon.

depends on sorry what this means
Statement uses: Iff, True, AddCommGroup, Fintype, Exists, Finset, And, Green31.IsGroupSidon, LE.le, Real, HMul.hMul, OfScientific.ofScientific, Bool.true, Real.sqrt, Fintype.card, Finset.card
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_31.variants.abelian : answer(sorry) ↔
    ∀ (G : Type) [AddCommGroup G] [Fintype G],
      ∃ S : Finset G, IsGroupSidon (S : Set G) ∧
        0.01 * Real.sqrt (Fintype.card G) ≤ S.card := by
…
```
Mentions: Green31.IsGroupSidon
def Green31.IsBinarySidon A set of binary vectors is Sidon if its pairwise sums, taken coordinatewise in ℕ, determine the unordered pair of summands line 214 source
Source documentation
A set of binary vectors is Sidon if its pairwise sums, taken coordinatewise in ℕ, determine the unordered pair of summands.

no axioms what this means
Statement uses: Nat, Set, 𝔽₂
Proof uses: Membership.mem, Eq, Fin, HAdd.hAdd, ZMod.val, OfNat.ofNat, Or, And
4 instances, coercions and auxiliary constants left out.
```
def IsBinarySidon {n : ℕ} (S : Set (𝔽₂ n)) : Prop :=
…
```
Mentions: 𝔽₂
theorem Green31.green_31.variants.sidon_01n Another very nice old problem is whether there is a Sidon subset of $\{0, 1\}^n$ of size $N^{0.51}$, where $N = 2^n$ [Gr24] sorry line 224 source
Source documentation
Another very nice old problem is whether there is a Sidon subset of $\{0, 1\}^n$ of size $N^{0.51}$, where $N = 2^n$ [Gr24].

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Finset, 𝔽₂, And, Green31.IsBinarySidon, Filter.Eventually, LE.le, Real, HPow.hPow, OfNat.ofNat, OfScientific.ofScientific, Bool.true, Finset.card, Filter.atTop
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 green_31.variants.sidon_01n : answer(sorry) ↔
    ∃ S : (n : ℕ) → Finset (𝔽₂ n),
      (∀ n, IsBinarySidon (S n : Set (𝔽₂ n))) ∧
      ∀ᶠ n in atTop, ((2 : ℝ) ^ n) ^ (0.51 : ℝ) ≤ (S n).card := by
…
```
Mentions: 𝔽₂, Green31.IsBinarySidon
theorem Green31.green_31.variants.sidon_01n_clz01 The best-known upper bound for a Sidon subset of $\{0, 1\}^n$ ($N = 2^n$) is $N^{0.5753}$ [CLZ01] sorry line 234 source
Source documentation
The best-known upper bound for a Sidon subset of $\{0, 1\}^n$ ($N = 2^n$) is $N^{0.5753}$ [CLZ01].

depends on sorry what this means
Statement uses: Exists, Real, Nat, Finset, 𝔽₂, Green31.IsBinarySidon, LE.le, Finset.card, HMul.hMul, HPow.hPow, OfNat.ofNat, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_31.variants.sidon_01n_clz01 :
    ∃ C : ℝ, ∀ n, ∀ S : Finset (𝔽₂ n),
      IsBinarySidon (S : Set (𝔽₂ n)) →
        (S.card : ℝ) ≤ C * ((2 : ℝ) ^ n) ^ (0.5753 : ℝ) := by
…
```
Mentions: 𝔽₂, Green31.IsBinarySidon