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

10 declarations, 9 contain sorry, 0 declared as axioms

Erdős Problem 30

References:

erdosproblems.com/30
[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. 16 (1941), 212-215.
[Li69] Lindström, B., An inequality for $B_2$-sequences. J. Combinatorial Theory 6 (1969), 211-212.
[Si38] Singer, J., A theorem in finite projective geometry and some applications to number theory. Trans. Amer. Math. Soc. 43 (1938), 377-385.
[BFR23] Balogh, J., Füredi, Z. and Roy, S., An upper bound on the size of Sidon sets. Amer. Math. Monthly 130 (2023), 437-445.
[OB22] O'Bryant, K., On the size of finite Sidon sets. arXiv:2207.07800 (2022).
[CHO25] Carter, D., Hunter, Z. and O'Bryant, K., On the diameter of finite Sidon sets. Acta Math. Hungar. 175 (2025), 108-126.

See also Ben Green's Open Problem 31 (formalised in FormalConjectures/GreensOpenProblems/31.lean).

Imports (1)

FormalConjecturesUtil

abbrev Erdos30.h Let $h(N)$ be the maximum size of a Sidon set in $\{1, \dots, N\}$ line 49 source
Source documentation
Let $h(N)$ be the maximum size of a Sidon set in $\{1, \dots, N\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.maxSidonSubsetCard, Finset.Icc, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev h (N : ℕ) : ℕ := Finset.maxSidonSubsetCard (Finset.Icc 1 N)
…
```
Mentions: Finset.maxSidonSubsetCard
theorem Erdos30.erdos_30 Is it true that, for every $\varepsilon > 0$, $h(N) = \sqrt N + O_{\varepsilon}(N^\varepsilon)$ sorry line 59 source
Source documentation
Is it true that, for every $\varepsilon > 0$, $h(N) = \sqrt N + O_{\varepsilon}(N^\varepsilon)$

depends on sorry what this means
Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Asymptotics.IsBigO, Nat, Filter.atTop, HSub.hSub, Erdos30.h, Real.sqrt, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_30 : answer(sorry) ↔
    ∀ᵉ (ε > 0), (fun N => h N - (N : Real).sqrt) =O[atTop] fun N => (N : ℝ)^(ε : ℝ) := by
…
```
Mentions: Erdos30.h
theorem Erdos30.erdos_30.variants.O_one A stronger conjecture: is it true that $h(N) = \sqrt N + O(1)$? sorry line 68 source
Source documentation
A stronger conjecture: is it true that $h(N) = \sqrt N + O(1)$? Erdős thought this was perhaps too optimistic.

depends on sorry what this means
Statement uses: Iff, True, Asymptotics.IsBigO, Nat, Real, Filter.atTop, HSub.hSub, Erdos30.h, Real.sqrt, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_30.variants.O_one : answer(sorry) ↔
    (fun N => h N - (N : ℝ).sqrt) =O[atTop] fun _ => (1 : ℝ) := by
…
```
Mentions: Erdos30.h
theorem Erdos30.erdos_30.variants.erdos_turan Erdős and Turán [ErTu41] proved $h(N) \le \sqrt N + O(N^{1/4})$ sorry line 76 source
Source documentation
Erdős and Turán [ErTu41] proved $h(N) \le \sqrt N + O(N^{1/4})$.

depends on sorry what this means
Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HSub.hSub, Erdos30.h, Real.sqrt, HPow.hPow, Inv.inv, OfNat.ofNat
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 erdos_30.variants.erdos_turan :
    (fun N => h N - (N : ℝ).sqrt) =O[atTop] fun N => (N : ℝ) ^ (4⁻¹ : ℝ) := by
…
```
Mentions: Erdos30.h
theorem Erdos30.erdos_30.variants.lindstrom The proofs of Erdős–Turán [ErTu41] and Lindström [Li69] in fact give, for all $N$, $h(N) \le N^{1/2} + N^{1/4} + 1$ sorry line 85 source
Source documentation
The proofs of Erdős–Turán [ErTu41] and Lindström [Li69] in fact give, for all $N$, $h(N) \le N^{1/2} + N^{1/4} + 1$.

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_30.variants.lindstrom (N : ℕ) :
    (h N : ℝ) ≤ (N : ℝ).sqrt + (N : ℝ) ^ (4⁻¹ : ℝ) + 1 := by
…
```
Mentions: Erdos30.h
theorem Erdos30.erdos_30.variants.balogh_furedi_roy Balogh, Füredi and Roy [BFR23] proved $h(N) \le N^{1/2} + 0.998 N^{1/4}$ for all sufficiently large $N$ sorry line 94 source
Source documentation
Balogh, Füredi and Roy [BFR23] proved $h(N) \le N^{1/2} + 0.998 N^{1/4}$ for all sufficiently large $N$.

depends on sorry what this means
Statement uses: Filter.Eventually, Nat, LE.le, Real, Erdos30.h, 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 erdos_30.variants.balogh_furedi_roy :
    ∀ᶠ N in atTop, (h N : ℝ) ≤ (N : ℝ).sqrt + (0.998 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ) := by
…
```
Mentions: Erdos30.h
theorem Erdos30.erdos_30.variants.obryant O'Bryant [OB22] proved $h(N) \le N^{1/2} + 0.99703 N^{1/4}$ for all sufficiently large $N$ sorry line 102 source
Source documentation
O'Bryant [OB22] proved $h(N) \le N^{1/2} + 0.99703 N^{1/4}$ for all sufficiently large $N$.

depends on sorry what this means
Statement uses: Filter.Eventually, Nat, LE.le, Real, Erdos30.h, 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 erdos_30.variants.obryant :
    ∀ᶠ N in atTop, (h N : ℝ) ≤ (N : ℝ).sqrt + (0.99703 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ) := by
…
```
Mentions: Erdos30.h
theorem Erdos30.erdos_30.variants.carter_hunter_obryant Carter, Hunter and O'Bryant [CHO25] proved $h(N) \le N^{1/2} + 0.98183 N^{1/4} + O(1)$ sorry line 111 source
Source documentation
Carter, Hunter and O'Bryant [CHO25] proved $h(N) \le N^{1/2} + 0.98183 N^{1/4} + O(1)$. This is the current record upper bound.

depends on sorry what this means
Statement uses: Exists, Real, Filter.Eventually, Nat, LE.le, Erdos30.h, 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 erdos_30.variants.carter_hunter_obryant :
    ∃ C : ℝ, ∀ᶠ N in atTop,
      (h N : ℝ) ≤ (N : ℝ).sqrt + (0.98183 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ) + C := by
…
```
Mentions: Erdos30.h
theorem Erdos30.erdos_30.variants.singer Singer's construction [Si38] shows $h(N) \ge (1 - o(1)) N^{1/2}$ for all $N$ sorry line 120 source
Source documentation
Singer's construction [Si38] shows $h(N) \ge (1 - o(1)) N^{1/2}$ for all $N$.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, HMul.hMul, HSub.hSub, Real.sqrt, Erdos30.h, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_30.variants.singer :
    ∀ ε > (0 : ℝ), ∀ᶠ N : ℕ in atTop, (1 - ε) * (N : ℝ).sqrt ≤ h N := by
…
```
Mentions: Erdos30.h
theorem Erdos30.erdos_30.variants.isEquivalent_sqrt Combining Singer's lower bound [Si38] with the Erdős–Turán upper bound [ErTu41]: $h(N) \sim N^{1/2}$ sorry line 129 source
Source documentation
Combining Singer's lower bound [Si38] with the Erdős–Turán upper bound [ErTu41]: $h(N) \sim N^{1/2}$.

depends on sorry what this means
Statement uses: Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, Erdos30.h, Real.sqrt
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_30.variants.isEquivalent_sqrt :
    (fun N => (h N : ℝ)) ~[atTop] fun N => (N : ℝ).sqrt := by
…
```
Mentions: Erdos30.h