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

References:

erdosproblems.com/30
erdosproblems.com/241
[BoCh62] Bose, R. C. and Chowla, S., Theorems in the additive theory of numbers. Comment. Math. Helv. (1962/63), 141-147.
[Gr01] Green, Ben, The number of squares and {$B_h[g]$} sets. Acta Arith. (2001), 365-390.
[Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
[Wh24] White, Ethan Patrick, An optimal $L^2$ autoconvolution inequality. Canad. Math. Bull. 67 (2024), 108-121. doi:10.4153/S0008439523000565

Imports (1)

FormalConjecturesUtil

def Erdos241.f Let $f(N)$ be the maximum size of $A\subseteq \{1,\ldots,N\}$ such that the sums $a+b+c$ with $a,b,c\in A$ are all distinct (aside from the trivial coincidences) line 47 source
Source documentation
Let $f(N)$ be the maximum size of $A\subseteq \{1,\ldots,N\}$ such that the sums $a+b+c$ with $a,b,c\in A$ are all distinct (aside from the trivial coincidences).
Formalization note: this is generalized to allow for different $r$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sup, Finset, Finset.filter, Multiset, Eq, Multiset.card, Membership.mem, Multiset.sum, Classical.propDecidable, Finset.powerset, Finset.Icc, OfNat.ofNat, Finset.card
10 instances, coercions and auxiliary constants left out.
```
noncomputable def f (N r : ℕ) : ℕ :=
…
```
theorem Erdos241.erdos_241 Is it true that $f(N)\sim N^{1/3}$? sorry line 64 source
Source documentation
Is it true that $f(N)\sim N^{1/3}$?
Originally asked to Erdős by Bose.
This is discussed in problem C11 of Guy's collection [Gu04].

depends on sorry what this means
Statement uses: Iff, True, Asymptotics.IsEquivalent, Nat, Real, Filter.atTop, Erdos241.f, OfNat.ofNat, HPow.hPow, HDiv.hDiv
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_241 :
    answer(sorry) ↔ (fun N ↦ (f N 3 : ℝ)) ~[atTop] (fun N ↦ (N : ℝ) ^ ((1 : ℝ) / 3)) := by
…
```
Mentions: Erdos241.f
theorem Erdos241.erdos_241.variants.lower_bound Bose and Chowla [BoCh62] provided a construction proving one half of this, namely $(1+o(1))N^{1/3}\leq f(N)$ sorry line 73 source
Source documentation
Bose and Chowla [BoCh62] provided a construction proving one half of this, namely $(1+o(1))N^{1/3}\leq f(N)$.

depends on sorry what this means
Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, LE.le, HMul.hMul, HAdd.hAdd, HPow.hPow, HDiv.hDiv, Erdos241.f
Proof uses: sorryAx, Lean.Name, Bool.false, 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 erdos_241.variants.lower_bound :
    ∃ ε : ℕ → ℝ, ε =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
    ∀ᶠ N in atTop, (1 + ε N) * (N : ℝ) ^ ((1 : ℝ) / 3) ≤ (f N 3 : ℝ) := by
…
```
Mentions: Erdos241.f
theorem Erdos241.erdos_241.variants.upper_bound Green [Gr01] proved the upper bound $f(N) \leq ((7/2)^{1/3}+o(1))N^{1/3}$ (note that $(7/2)^{1/3}\approx 1.519$) sorry line 83 source
Source documentation
Green [Gr01] proved the upper bound $f(N) \leq ((7/2)^{1/3}+o(1))N^{1/3}$ (note that $(7/2)^{1/3}\approx 1.519$).

depends on sorry what this means
Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, LE.le, Erdos241.f, HMul.hMul, HAdd.hAdd, HPow.hPow, HDiv.hDiv
Proof uses: sorryAx, Lean.Name, Bool.false, 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 erdos_241.variants.upper_bound :
    ∃ ε : ℕ → ℝ, ε =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
    ∀ᶠ N in atTop, (f N 3 : ℝ) ≤ ((7 / 2 : ℝ) ^ ((1 : ℝ) / 3) + ε N) * (N : ℝ) ^ ((1 : ℝ) / 3) := by
…
```
Mentions: Erdos241.f
theorem Erdos241.erdos_241.variants.upper_bound_white Green's argument gives sorry line 96 source
Source documentation
Green's argument gives $f(N) \leq ((2/\mu_2^2)^{1/3}+o(1))N^{1/3}$, where $\mu_2^2 = \inf \lVert g \ast g \rVert_2^2$ over $g \colon [-1/2,1/2] \to \mathbb{R}$ with $\int g = 1$; Green used $\mu_2^2 \geq 4/7$. White [Wh24, Theorem 1 and Corollary 2] proved $0.574636066 \leq \mu_2^2 \leq 0.574642912$, which gives the best upper bound known to date, $f(N) \leq ((2/0.574636066)^{1/3}+o(1))N^{1/3}$ (note that $(2/0.574636066)^{1/3}\approx 1.5155$).

depends on sorry what this means
Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, LE.le, Erdos241.f, HMul.hMul, HAdd.hAdd, HPow.hPow, HDiv.hDiv, OfScientific.ofScientific, Bool.true
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_241.variants.upper_bound_white :
    ∃ ε : ℕ → ℝ, ε =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
    ∀ᶠ N in atTop, (f N 3 : ℝ) ≤
      ((2 / 0.574636066 : ℝ) ^ ((1 : ℝ) / 3) + ε N) * (N : ℝ) ^ ((1 : ℝ) / 3) := by
…
```
Mentions: Erdos241.f
def Erdos241.BoseChowlaConjecture The conjecture that the size of the set $A\subseteq \{1,\ldots,N\}$ is asymptotically $N^{1/r}$ line 105 source
Source documentation
The conjecture that the size of the set $A\subseteq \{1,\ldots,N\}$ is asymptotically $N^{1/r}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Asymptotics.IsEquivalent, Real, Filter.atTop, Erdos241.f, HPow.hPow, HDiv.hDiv, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.
```
def BoseChowlaConjecture (r : ℕ) : Prop :=
…
```
theorem Erdos241.erdos_241.variants.generalization Documented declaration: generalization sorry line 114 source
Source documentation
More generally, Bose and Chowla [BoCh62] conjectured that the maximum size of $A\subseteq \{1,\ldots,N\}$ with all $r$-fold sums distinct (aside from the trivial coincidences) then $\lvert A\rvert \sim N^{1/r}.$

depends on sorry what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Erdos241.BoseChowlaConjecture
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_241.variants.generalization (r : ℕ) (hr : r ≥ 2) :  BoseChowlaConjecture r := by
…
```
Mentions: Erdos241.BoseChowlaConjecture
theorem Erdos241.erdos_241.variants.r_eq_2 This is known only for $r=2$ (see [erdosproblems.com/30]) sorry line 121 source
Source documentation
This is known only for $r=2$ (see [erdosproblems.com/30]).

depends on sorry what this means
Statement uses: Erdos241.BoseChowlaConjecture, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_241.variants.r_eq_2 :
    BoseChowlaConjecture 2 := by
…
```
Mentions: Erdos241.BoseChowlaConjecture