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

12 declarations, 9 contain sorry, 0 declared as axioms

Erdős Problem 138

References:

erdosproblems.com/138
[Be68] Berlekamp, E. R., A construction for partitions which avoid long arithmetic progressions. Canad. Math. Bull. (1968), 409-414.
[Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
[Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42.
[Go01] Gowers, W. T., A new proof of Szemerédi's theorem. Geom. Funct. Anal. (2001), 465-588.
arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.
[CFS26] Campos, M., Fox, J. and Schildkraut, C., A new lower bound for two-color van der Waerden numbers. arXiv:2608.20824 (2026).

Imports (1)

FormalConjecturesUtil

def Erdos138.monoAP_guarantee_set The set of natural numbers that guarantee a monochromatic arithmetic progression line 49 source
Source documentation
The set of natural numbers that guarantee a monochromatic arithmetic progression.
A number N belongs to this set if, for a given number of colors r and an arithmetic progression length k, any r-coloring of the integers {1, ..., N} must contain a monochromatic arithmetic progression of length k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set
Proof uses: Set.ofPred, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Fin, ContainsMonoAPofLength
8 instances, coercions and auxiliary constants left out.
```
def monoAP_guarantee_set (r k : ℕ) : Set ℕ :=
…
```
theorem Erdos138.monoAP_guarantee_set_nonempty Asserts that for any number of colors r and any progression length k, there always exists some number N large enough to guarantee a monochromatic arithmetic progression sorry line 59 source
Source documentation
Asserts that for any number of colors r and any progression length k, there always exists some number N large enough to guarantee a monochromatic arithmetic progression. In other words, the set monoAP_guarantee_set is non-empty. This is the fundamental existence result that allows for the definition of the van der Waerden numbers.

depends on sorry what this means
Statement uses: Nat, Set.Nonempty, Erdos138.monoAP_guarantee_set
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem monoAP_guarantee_set_nonempty (r k) : (monoAP_guarantee_set r k).Nonempty := by
…
```
Mentions: Erdos138.monoAP_guarantee_set
def Erdos138.monoAPNumber The van der Waerden number, is the smallest integer N such that any r-coloring of {1, ..., N} is guaranteed to contain a monochromatic arithmetic progression of length k line 67 source
Source documentation
The van der Waerden number, is the smallest integer N such that any r-coloring of {1, ..., N} is guaranteed to contain a monochromatic arithmetic progression of length k. It is defined as the infimum of the (non-empty) set of all such numbers N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Erdos138.monoAP_guarantee_set
1 instances, coercions and auxiliary constants left out.
```
noncomputable def monoAPNumber (r k : ℕ) : ℕ := sInf (monoAP_guarantee_set r k)
```
Mentions: Erdos138.monoAP_guarantee_set
abbrev Erdos138.W An abbreviation for the van der Waerden number for 2 colors, commonly written as W(k) line 74 source
Source documentation
An abbreviation for the van der Waerden number for 2 colors, commonly written as W(k). This represents the smallest integer N such that any 2-coloring of {1, ..., N} must contain a monochromatic arithmetic progression of length k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Erdos138.monoAPNumber, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev W : ℕ → ℕ := monoAPNumber 2
…
```
Mentions: Erdos138.monoAPNumber
theorem Erdos138.monoAPNumber_two_one sorry line 78 source
depends on sorry what this means
Statement uses: Eq, Nat, Erdos138.W, OfNat.ofNat
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 Erdos138.monoAPNumber_two_two sorry line 83 source
depends on sorry what this means
Statement uses: Eq, Nat, Erdos138.W, OfNat.ofNat
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 Erdos138.erdos_138 In [Er80] Erdős asks whether $$ \lim_{k \to \infty} (W(k))^{1/k} = \infty $$ sorry line 91 source
Source documentation
In [Er80] Erdős asks whether $$ \lim_{k \to \infty} (W(k))^{1/k} = \infty $$

depends on sorry what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, Real, HPow.hPow, Erdos138.W, HDiv.hDiv, OfNat.ofNat, Filter.atTop
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_138 : answer(sorry) ↔ atTop.Tendsto (fun k => (W k : ℝ)^(1/(k : ℝ))) atTop := by
…
```
Mentions: Erdos138.W
theorem Erdos138.erdos_138.variants.prime When $p$ is prime Berlekamp [Be68] has proved $W(p+1) ≥ p^{2^p}$ sorry line 99 source
Source documentation
When $p$ is prime Berlekamp [Be68] has proved $W(p+1) ≥ p^{2^p}$.

depends on sorry what this means
Statement uses: Nat, Nat.Prime, LE.le, HMul.hMul, HPow.hPow, OfNat.ofNat, Erdos138.W, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_138.variants.prime (p : ℕ) (hp : p.Prime) : p * (2 ^ p) ≤ W (p + 1) := by
…
```
Mentions: Erdos138.W
theorem Erdos138.erdos_138.variants.upper Gowers [Go01] has proved $$W(k) \leq 2^{2^{2^{2^{2^{k+9}}}}.$$ sorry line 106 source
Source documentation
Gowers [Go01] has proved $$W(k) \leq 2^{2^{2^{2^{2^{k+9}}}}.$$

depends on sorry what this means
Statement uses: Nat, LE.le, Erdos138.W, HPow.hPow, OfNat.ofNat, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_138.variants.upper (k : ℕ) : W k ≤ 2 ^ (2 ^ (2 ^ 2 ^ 2 ^ (k + 9))) := by
…
```
Mentions: Erdos138.W
theorem Erdos138.erdos_138.variants.quotient In [Er81] Erdős asks whether $\frac{W(k+1)}{W(k)} \to \infty$ sorry line 113 source
Source documentation
In [Er81] Erdős asks whether $\frac{W(k+1)}{W(k)} \to \infty$.

depends on sorry what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, Rat, HDiv.hDiv, Erdos138.W, HAdd.hAdd, OfNat.ofNat, Filter.atTop
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_138.variants.quotient :
    answer(sorry) ↔ atTop.Tendsto (fun k => ((W (k + 1) : ℚ)/(W k))) atTop := by
…
```
Mentions: Erdos138.W
theorem Erdos138.erdos_138.variants.difference sorry line 124 source
depends on sorry what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, HSub.hSub, Erdos138.W, HAdd.hAdd, OfNat.ofNat, Filter.atTop
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 Erdos138.erdos_138.variants.dvd_two_pow sorry line 143 source
depends on sorry what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, Rat, HDiv.hDiv, Erdos138.W, HPow.hPow, OfNat.ofNat, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.