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

Green's Open Problem 25

References:

[Gr24] Green, Ben. "100 open problems." (2024).
[ESS89] Erdős, Pál, András Sárközy, and V. T. Sós. "On a conjecture of Roth and some related problems I." Irregularities of partitions. Berlin, Heidelberg: Springer Berlin Heidelberg, 1989. 47-59.
[Ru04] Ruzsa, Imre Z. "A problem on restricted sumsets." CONTEMPORARY MATHEMATICS 342 (2004): 245-248.

Imports (1)

FormalConjecturesUtil

def Green25.Property25 For which values of $k$ is the following true: whenever we partition $[N] = A_1 \cup \dots \cup A_k$, $\left|\bigcup^k_{i=1} (A_i \hat{+} A_i)\right| \geq \frac{1}{10} N$? line 42 source
Source documentation
For which values of $k$ is the following true: whenever we partition $[N] = A_1 \cup \dots \cup A_k$, $\left|\bigcup^k_{i=1} (A_i \hat{+} A_i)\right| \geq \frac{1}{10} N$?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, LE.le, OfNat.ofNat, Finpartition, Finset, Finset.Icc, Eq, Finset.card, Finpartition.parts, GE.ge, HMul.hMul, Finset.biUnion, Finset.restrictedSumset
10 instances, coercions and auxiliary constants left out.
```
def Property25 (k N : ℕ) : Prop :=
…
```
def Green25.bestLower The best-known lower bound [ESS89] line 48 source
Source documentation
The best-known lower bound [ESS89].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Real.log
2 instances, coercions and auxiliary constants left out.
```
noncomputable def bestLower (N : ℕ) : ℝ := Real.log (Real.log N)
```
def Green25.bestUpper The best-known upper bound [ESS89] line 51 source
Source documentation
The best-known upper bound [ESS89].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, Real.log
5 instances, coercions and auxiliary constants left out.
```
noncomputable def bestUpper (N : ℕ) : ℝ := (N : ℝ) / Real.log N
…
```
theorem Green25.green_25 For which values of $k$ is the following true: whenever we partition $[N] = A_1 \cup \dots \cup A_k$, $\left|\bigcup^k_{i=1} (A_i \hat{+} A_i)\right| \geq \frac{1}{10} N$? sorry line 58 source
Source documentation
For which values of $k$ is the following true: whenever we partition $[N] = A_1 \cup \dots \cup A_k$, $\left|\bigcup^k_{i=1} (A_i \hat{+} A_i)\right| \geq \frac{1}{10} N$?

depends on sorry what this means
Statement uses: Eq, Set, Nat, Set.ofPred, Filter.Eventually, Green25.Property25, Filter.atTop, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_25 : {k : ℕ → ℕ | ∀ᶠ N in atTop, Property25 (k N) N} = answer(sorry) := by
…
```
Mentions: Green25.Property25
theorem Green25.green_25.upper We conjecture that the best-known upper bound can be lowered sorry line 63 source
Source documentation
We conjecture that the best-known upper bound can be lowered.

depends on sorry what this means
Statement uses: Nat, sorryAx, Bool.false, And, Filter.Eventually, LE.le, OfNat.ofNat, Filter.atTop, Asymptotics.IsLittleO, Real, Green25.bestUpper, Not, Green25.Property25
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_25.upper :
    let ans := (answer(sorry) : ℕ → ℕ)
…
```
theorem Green25.green_25.lower We conjecture that the best-known lower bound can be raised sorry line 72 source
Source documentation
We conjecture that the best-known lower bound can be raised.

depends on sorry what this means
Statement uses: Nat, Real, sorryAx, Bool.false, And, Asymptotics.IsLittleO, Filter.atTop, Green25.bestLower, Filter.Eventually, LE.le, OfNat.ofNat, Asymptotics.IsBigO, Green25.Property25
Proof uses: Lean.Name, 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 green_25.lower :
    let ans := (answer(sorry) : ℕ → ℝ)
…
```
theorem Green25.green_25.variants.lower_ess89 For $k \ll \log \log N$, this is true [Gr24] sorry line 89 source
Source documentation
For $k \ll \log \log N$, this is true [Gr24].
NOTE: [ESS89] derive a precise constant for which this is true, but $\ll$ would imply that it works for any constant. We thus prefer a little-o statement.

depends on sorry what this means
Statement uses: Nat, And, Filter.Eventually, LE.le, OfNat.ofNat, Filter.atTop, Asymptotics.IsLittleO, Real, Green25.bestLower, Green25.Property25
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_25.variants.lower_ess89 :
  ∀ k : ℕ → ℕ,
    (∀ᶠ N in atTop, 1 ≤ k N ∧ k N ≤ N) ∧ -- Ensure Property25 is not False due to non-existent partitions
    (fun N => (k N : ℝ)) =o[atTop] bestLower →
    ∀ᶠ N in atTop, Property25 (k N) N := by
…
```
Mentions: Green25.Property25, Green25.bestLower
theorem Green25.green_25.variants.upper_ess89 For $k \gg N / \log N$, it need not be true [Gr24] sorry line 103 source
Source documentation
For $k \gg N / \log N$, it need not be true [Gr24].
We formalize by enforcing a $N / \log N$ growth rate on $k(N)$. This avoids cases like $k(N) = N$ or $N-1$, which produce trivial counter examples with singletons and thus empty restricted sumsets.

depends on sorry what this means
Statement uses: Exists, Nat, And, Filter.Eventually, LE.le, OfNat.ofNat, Filter.atTop, Asymptotics.IsTheta, Real, Green25.bestUpper, Not, Green25.Property25
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_25.variants.upper_ess89 :
  ∃ k : ℕ → ℕ,
    (∀ᶠ N in atTop, 1 ≤ k N ∧ k N ≤ N) ∧
    (fun N => (k N : ℝ)) =Θ[atTop] bestUpper ∧
    ¬ ∀ᶠ N in atTop, Property25 (k N) N := by
…
```
Mentions: Green25.bestUpper, Green25.Property25
theorem Green25.green_25.variants.upper_ess89_trivial For $k \gg N / \log N$, it need not be true [Gr24] sorry line 116 source
Source documentation
For $k \gg N / \log N$, it need not be true [Gr24].
In this version, cases like $k(N) = N$ or $N-1$ can produce trivial counter examples.

depends on sorry what this means
Statement uses: Exists, Nat, And, Filter.Eventually, LE.le, OfNat.ofNat, Filter.atTop, Asymptotics.IsBigO, Real, Green25.bestUpper, Not, Green25.Property25
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_25.variants.upper_ess89_trivial :
  ∃ k : ℕ → ℕ,
    (∀ᶠ N in atTop, 1 ≤ k N ∧ k N ≤ N) ∧
    ((fun N => (k N : ℝ)) ≫ bestUpper) ∧
    ¬ ∀ᶠ N in atTop, Property25 (k N) N := by
…
```
Mentions: Green25.bestUpper, Green25.Property25
theorem Green25.green_25.variants.upper_pow_23_40 sorry line 132 source
depends on sorry what this means
Statement uses: Nat, Nat.ceil, Real, HPow.hPow, HDiv.hDiv, OfNat.ofNat, And, Filter.Eventually, LE.le, Filter.atTop, Asymptotics.IsLittleO, Green25.bestUpper, Not, Green25.Property25
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.