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

60 declarations, 58 contain sorry, 0 declared as axioms

Ben Green's Open Problem 14

References:

[Gr24] Green, Ben. "100 open problems." (2024).
[AKS14] Ahmed, Tanbir, Oliver Kullmann, and Hunter Snevily. "On the van der Waerden numbers w (2; 3, t)." Discrete Applied Mathematics 174 (2014): 27-51.
[KeMe23] Kelley, Zander, and Raghu Meka. "Strong bounds for 3-progressions." 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS). IEEE, 2023.
[Hu22] Hunter, Zach. "Improved lower bounds for van der Waerden numbers." Combinatorica 42. Suppl 2 (2022): 1231-1252.
[Gr21] Green, Ben. "New lower bounds for van der Waerden numbers." Forum of Mathematics, Pi. Vol. 10. Cambridge University Press, 2022.
[Sc20] Schoen, Tomasz. "A subexponential upper bound for van der Waerden numbers W (3, k)." arXiv preprint arXiv:2006.02877 (2020).
[BLR08] Brown, Tom, Bruce M. Landman, and Aaron Robertson. "Bounds on some van der Waerden numbers." Journal of Combinatorial Theory, Series A 115.7 (2008): 1304-1309.
[LiSh10] Li, Yusheng, and Jinlong Shu. "A lower bound for off-diagonal van der Waerden numbers." Advances in Applied Mathematics 44.3 (2010): 243-247.
[Ko15] Kouril, Michal. "Leveraging FPGA clusters for SAT computations." Parallel Computing: On the Road to Exascale (2015): 525-532.
[CCH23] Chowdhury, Md Solimul, Cayden R. Codel, and Marijn J. H. Heule. "A linear weight transfer rule for local search." NASA Formal Methods (NFM 2023), Springer (2023).

Imports (1)

FormalConjecturesUtil

Imported by 2 files

def Green14.mixedMonoAPGuaranteeSet The set of natural numbers $N$ such that any 2-coloring of ${1, ..., N}$ contains a monochromatic arithmetic progression of length $k$ (color 0) or length $r$ (color 1) line 55 source
Source documentation
The set of natural numbers $N$ such that any 2-coloring of ${1, ..., N}$ contains a monochromatic arithmetic progression of length $k$ (color 0) or length $r$ (color 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set
Proof uses: Set.ofPred, Set.Icc, OfNat.ofNat, Fin, Or, Exists, Finset, And, Set.IsAPOfLength, Membership.mem, Eq, ENat
12 instances, coercions and auxiliary constants left out.
```
def mixedMonoAPGuaranteeSet (k r : ℕ) : Set ℕ :=
…
```
def Green14.W We define the 2-colour van der Waerden numbers line 65 source
Source documentation
We define the 2-colour van der Waerden numbers $W(k, r)$ to be the least quantities such that if $\{1, ... , W(k, r)\}$ is coloured red and blue then there is either a red $k$-term progression or a blue $r$-term progression.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Green14.mixedMonoAPGuaranteeSet
1 instances, coercions and auxiliary constants left out.
```
noncomputable def W (k r : ℕ) : ℕ := sInf (mixedMonoAPGuaranteeSet k r)
…
```
Mentions: Green14.mixedMonoAPGuaranteeSet
theorem Green14.green_14_polynomial Is $W(k, r)$ a polynomial in $r$, for fixed $k$? sorry line 78 source
Source documentation
Is $W(k, r)$ a polynomial in $r$, for fixed $k$?
We formulate this as asking if $W(k, r)$ has polynomial growth in $r$. The answer is no, already for $k = 4$. Every red $k$-term progression with $k \ge 3$ contains a red $3$-term progression, so mixedMonoAPGuaranteeSet k r ⊆ mixedMonoAPGuaranteeSet 3 r, and both sets are nonempty by van der Waerden's theorem, so $W(3, r) \le W(k, r)$. Polynomial growth for one $k \ge 4$ would therefore force polynomial growth for $k = 3$, contradicting green_14_polynomial_k_eq_3 [Gr21, p.3].

depends on sorry what this means
Statement uses: Iff, False, Nat, GE.ge, OfNat.ofNat, Exists, Asymptotics.IsBigO, Real, Filter.atTop, Green14.W, HPow.hPow
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 green_14_polynomial :
    answer(False) ↔ ∀ k ≥ 4, ∃ d : ℕ, (fun r => (W k r : ℝ)) =O[atTop] fun r => (r : ℝ) ^ d := by
…
```
Mentions: Green14.W
theorem Green14.green_14_polynomial_k_eq_3 We know $W(3, r)$ does not have polynomial growth in $r$ [Gr21, p.3] sorry line 84 source
Source documentation
We know $W(3, r)$ does not have polynomial growth in $r$ [Gr21, p.3].

depends on sorry what this means
Statement uses: Not, Exists, Nat, Asymptotics.IsBigO, Real, Filter.atTop, Green14.W, OfNat.ofNat, HPow.hPow
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 green_14_polynomial_k_eq_3 :
    ¬ ∃ d : ℕ, (fun r => (W 3 r : ℝ)) =O[atTop] fun r => (r : ℝ) ^ d := by
…
```
Mentions: Green14.W
theorem Green14.green_14_quadratic Is $W(3, r) \ll r^2$? sorry line 94 source
Source documentation
Is $W(3, r) \ll r^2$?
[Gr21] proves a superpolynomial lower bound $W(3, r) \gg \exp(c(\log r)^{4/3-o(1)})$.

depends on sorry what this means
Statement uses: Iff, False, Asymptotics.IsBigO, Nat, Real, Filter.atTop, Green14.W, OfNat.ofNat, HPow.hPow
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 green_14_quadratic :
    answer(False) ↔ (fun r => (W 3 r : ℝ)) =O[atTop] fun r => (r : ℝ) ^ 2 := by
…
```
Mentions: Green14.W
theorem Green14.green_14_lower_bound_green [Gr21] proved a lower bound of shape $W(3, r) \gg \exp(c(\log r)^{4/3-o(1)})$ sorry line 100 source
Source documentation
[Gr21] proved a lower bound of shape $W(3, r) \gg \exp(c(\log r)^{4/3-o(1)})$.

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, LT.lt, OfNat.ofNat, Nat, Filter.Tendsto, Filter.atTop, nhds, Asymptotics.IsBigO, Real.exp, HMul.hMul, HPow.hPow, Real.log, HSub.hSub, HDiv.hDiv, Green14.W
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_14_lower_bound_green :
    answer(True) ↔ ∃ c : ℝ, 0 < c ∧ ∃ (o : ℕ → ℝ) (_ : Tendsto o atTop (𝓝 0)),
    (fun (r : ℕ) => Real.exp (c * (Real.log r)^(4/3 - o r))) =O[atTop] fun r => (W 3 r : ℝ) := by
…
```
Mentions: c, Green14.W
theorem Green14.green_14_lower_bound_hunter [Hu22] improved this to $W(3, r) \gg \exp(c(\log r)^{2-o(1)})$ sorry line 107 source
Source documentation
[Hu22] improved this to $W(3, r) \gg \exp(c(\log r)^{2-o(1)})$.

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, LT.lt, OfNat.ofNat, Nat, Filter.Tendsto, Filter.atTop, nhds, Asymptotics.IsBigO, Real.exp, HMul.hMul, HPow.hPow, Real.log, HSub.hSub, Green14.W
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 green_14_lower_bound_hunter :
    answer(True) ↔ ∃ c : ℝ, 0 < c ∧ ∃ (o : ℕ → ℝ) (_ : Tendsto o atTop (𝓝 0)),
    (fun (r : ℕ) => Real.exp (c * (Real.log r)^(2 - o r))) =O[atTop] (fun r => (W 3 r : ℝ)) := by
…
```
Mentions: c, Green14.W
theorem Green14.green_14_lower_bound_brown_landman_robertson [BLR08] proved $W(3, r) \gg r^{2 - 1/\log \log r}$ sorry line 114 source
Source documentation
[BLR08] proved $W(3, r) \gg r^{2 - 1/\log \log r}$.

depends on sorry what this means
Statement uses: Iff, True, Asymptotics.IsBigO, Nat, Real, Filter.atTop, HPow.hPow, HSub.hSub, OfNat.ofNat, HDiv.hDiv, Real.log, Green14.W
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_14_lower_bound_brown_landman_robertson :
    answer(True) ↔
    (fun (r : ℕ) => (r : ℝ)^(2 - 1 / Real.log (Real.log r))) =O[atTop] (fun r => (W 3 r : ℝ)) := by
…
```
Mentions: Green14.W
theorem Green14.green_14_lower_bound_li_shu [LiSh10] proved $W(3, r) \gg (r / \log r)^2$ sorry line 121 source
Source documentation
[LiSh10] proved $W(3, r) \gg (r / \log r)^2$.

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_14_lower_bound_li_shu :
    answer(True) ↔
    (fun (r : ℕ) => ((r : ℝ) / Real.log r)^2) =O[atTop] (fun r => (W 3 r : ℝ)) := by
…
```
Mentions: Green14.W
theorem Green14.green_14_upper_bound_schoen [Sc20] proves the upper bound $W(3, r) < \exp(r^{1-c})$ for some $c > 0$ sorry line 128 source
Source documentation
[Sc20] proves the upper bound $W(3, r) < \exp(r^{1-c})$ for some $c > 0$.

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, LT.lt, OfNat.ofNat, Asymptotics.IsBigO, Nat, Filter.atTop, Green14.W, Real.exp, HPow.hPow, HSub.hSub
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 green_14_upper_bound_schoen :
    answer(True) ↔ ∃ c : ℝ, 0 < c ∧
    (fun (r : ℕ) => ((W 3 r) : ℝ)) =O[atTop] (fun r => Real.exp ((r : ℝ) ^ (1 - c))) := by
…
```
Mentions: c, Green14.W
theorem Green14.green_14_upper_bound_kelley_meka [KeMe23] gives a corresponding upper bound $W(3, r) \ll \exp(C(\log r)^C)$ sorry line 135 source
Source documentation
[KeMe23] gives a corresponding upper bound $W(3, r) \ll \exp(C(\log r)^C)$.

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, Asymptotics.IsBigO, Nat, Filter.atTop, Green14.W, OfNat.ofNat, Real.exp, HMul.hMul, HPow.hPow, Real.log
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 green_14_upper_bound_kelley_meka :
    answer(True) ↔ ∃ C : ℝ,
    (fun (r : ℕ) => ((W 3 r) : ℝ)) =O[atTop] (fun r => Real.exp (C * (Real.log r)^C)) := by
…
```
Mentions: Green14.W
theorem Green14.green_14_variant_2r2 It remains an interesting open problem to actually write down a colouring showing (say) $W(3, r) \ge 2r^2$ for some $r$ sorry line 145 source
Source documentation
It remains an interesting open problem to actually write down a colouring showing (say) $W(3, r) \ge 2r^2$ for some $r$. [Gr24]

depends on sorry what this means
Statement uses: Sigma, Nat, Set.Icc, OfNat.ofNat, HSub.hSub, HMul.hMul, HPow.hPow, Fin, sorryAx, Bool.false, Sigma.fst, Sigma.snd, And, LE.le, Not, Or, Exists, Finset, Set.IsAPOfLength, Set.ofPred and 4 more
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_14_variant_2r2 :
    -- Provide a pair (r, associated coloring) that avoids the monochromatic APs
    -- To show $W(3, r) > 2r^2 - 1$, we need a coloring of $\{1, \ldots, 2r^2 - 1\}$
    -- that avoids monochromatic APs of length 3 and $r$.
    let ans : Σ r : ℕ, Icc 1 (2 * r^2 - 1) → Fin 2 := answer(sorry)
…
```
Mentions: Green14.W
theorem Green14.W_3_3 sorry line 161 source
depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 Green14.W_3_4 sorry line 166 source
depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 Green14.W_3_5 sorry line 171 source
depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 Green14.W_3_6 $W(3, 6) = 32$ from [AKS14] sorry line 175 source
Source documentation
$W(3, 6) = 32$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_6 : W 3 6 = 32 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_7 $W(3, 7) = 46$ from [AKS14] sorry line 179 source
Source documentation
$W(3, 7) = 46$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_7 : W 3 7 = 46 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_8 $W(3, 8) = 58$ from [AKS14] sorry line 183 source
Source documentation
$W(3, 8) = 58$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_8 : W 3 8 = 58 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_9 $W(3, 9) = 77$ from [AKS14] sorry line 187 source
Source documentation
$W(3, 9) = 77$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_9 : W 3 9 = 77 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_10 $W(3, 10) = 97$ from [AKS14] sorry line 191 source
Source documentation
$W(3, 10) = 97$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_10 : W 3 10 = 97 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_11 $W(3, 11) = 114$ from [AKS14] sorry line 195 source
Source documentation
$W(3, 11) = 114$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_11 : W 3 11 = 114 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_12 $W(3, 12) = 135$ from [AKS14] sorry line 199 source
Source documentation
$W(3, 12) = 135$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_12 : W 3 12 = 135 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_13 $W(3, 13) = 160$ from [AKS14] sorry line 203 source
Source documentation
$W(3, 13) = 160$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_13 : W 3 13 = 160 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_14 $W(3, 14) = 186$ from [AKS14] sorry line 207 source
Source documentation
$W(3, 14) = 186$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_14 : W 3 14 = 186 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_15 $W(3, 15) = 218$ from [AKS14] sorry line 211 source
Source documentation
$W(3, 15) = 218$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_15 : W 3 15 = 218 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_16 $W(3, 16) = 238$ from [AKS14] sorry line 215 source
Source documentation
$W(3, 16) = 238$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_16 : W 3 16 = 238 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_17 $W(3, 17) = 279$ from [AKS14] sorry line 219 source
Source documentation
$W(3, 17) = 279$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_17 : W 3 17 = 279 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_18 $W(3, 18) = 312$ from [AKS14] sorry line 223 source
Source documentation
$W(3, 18) = 312$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_18 : W 3 18 = 312 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_19 $W(3, 19) = 349$ from [AKS14] sorry line 227 source
Source documentation
$W(3, 19) = 349$ from [AKS14].

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_19 : W 3 19 = 349 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_20_lower sorry line 235 source
depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
theorem Green14.W_3_20 $W(3, 20) = 389$, conjectured in [AKS14, Table 2] and established by Kouril [Ko15] using FPGA-based SAT solving sorry line 240 source
Source documentation
$W(3, 20) = 389$, conjectured in [AKS14, Table 2] and established by Kouril [Ko15] using FPGA-based SAT solving.

depends on sorry what this means
Statement uses: Eq, Nat, Green14.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 W_3_20 : W 3 20 = 389 := by sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_21_lower $W(3, 21) \ge 416$ from [AKS14, Table 2], proved by an explicit good partition sorry line 244 source
Source documentation
$W(3, 21) \ge 416$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_21_lower : answer(True) ↔ W 3 21 ≥ 416 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_21_eq [AKS14, Table 2] conjectures that $W(3, 21) = 416$ sorry line 248 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 21) = 416$.

depends on sorry what this means
Statement uses: Iff, True, Eq, Nat, Green14.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.
```
theorem W_3_21_eq : answer(sorry) ↔ W 3 21 = 416 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_22_lower $W(3, 22) \ge 464$ from [AKS14, Table 2], proved by an explicit good partition sorry line 252 source
Source documentation
$W(3, 22) \ge 464$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_22_lower : answer(True) ↔ W 3 22 ≥ 464 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_22_eq [AKS14, Table 2] conjectures that $W(3, 22) = 464$ sorry line 256 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 22) = 464$.

depends on sorry what this means
Statement uses: Iff, True, Eq, Nat, Green14.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.
```
theorem W_3_22_eq : answer(sorry) ↔ W 3 22 = 464 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_23_lower $W(3, 23) \ge 516$ from [AKS14, Table 2], proved by an explicit good partition sorry line 260 source
Source documentation
$W(3, 23) \ge 516$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_23_lower : answer(True) ↔ W 3 23 ≥ 516 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_23_eq [AKS14, Table 2] conjectures that $W(3, 23) = 516$ sorry line 264 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 23) = 516$.

depends on sorry what this means
Statement uses: Iff, True, Eq, Nat, Green14.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.
```
theorem W_3_23_eq : answer(sorry) ↔ W 3 23 = 516 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_24_lower $W(3, 24) \ge 593$ from [AKS14, Table 2], proved by an explicit good partition sorry line 268 source
Source documentation
$W(3, 24) \ge 593$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_24_lower : answer(True) ↔ W 3 24 ≥ 593 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_24_eq [AKS14, Table 2] conjectures that $W(3, 24) = 593$ sorry line 272 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 24) = 593$.

depends on sorry what this means
Statement uses: Iff, True, Eq, Nat, Green14.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.
```
theorem W_3_24_eq : answer(sorry) ↔ W 3 24 = 593 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_25_lower $W(3, 25) \ge 656$ from [AKS14, Table 2], proved by an explicit good partition sorry line 276 source
Source documentation
$W(3, 25) \ge 656$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_25_lower : answer(True) ↔ W 3 25 ≥ 656 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_25_eq [AKS14, Table 2] conjectures that $W(3, 25) = 656$ sorry line 280 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 25) = 656$.

depends on sorry what this means
Statement uses: Iff, True, Eq, Nat, Green14.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.
```
theorem W_3_25_eq : answer(sorry) ↔ W 3 25 = 656 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_26_lower $W(3, 26) \ge 727$ from [AKS14, Table 2], proved by an explicit good partition sorry line 284 source
Source documentation
$W(3, 26) \ge 727$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_26_lower : answer(True) ↔ W 3 26 ≥ 727 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_26_eq [AKS14, Table 2] conjectures that $W(3, 26) = 727$ sorry line 288 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 26) = 727$.

depends on sorry what this means
Statement uses: Iff, True, Eq, Nat, Green14.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.
```
theorem W_3_26_eq : answer(sorry) ↔ W 3 26 = 727 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_27_lower $W(3, 27) \ge 770$ from [AKS14, Table 2], proved by an explicit good partition sorry line 292 source
Source documentation
$W(3, 27) \ge 770$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_27_lower : answer(True) ↔ W 3 27 ≥ 770 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_27_eq [AKS14, Table 2] conjectures that $W(3, 27) = 770$ sorry line 296 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 27) = 770$.

depends on sorry what this means
Statement uses: Iff, True, Eq, Nat, Green14.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.
```
theorem W_3_27_eq : answer(sorry) ↔ W 3 27 = 770 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_28_lower $W(3, 28) \ge 827$ from [AKS14, Table 2], proved by an explicit good partition sorry line 300 source
Source documentation
$W(3, 28) \ge 827$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_28_lower : answer(True) ↔ W 3 28 ≥ 827 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_28_eq [AKS14, Table 2] conjectures that $W(3, 28) = 827$ sorry line 304 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 28) = 827$.

depends on sorry what this means
Statement uses: Iff, True, Eq, Nat, Green14.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.
```
theorem W_3_28_eq : answer(sorry) ↔ W 3 28 = 827 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_29_lower $W(3, 29) \ge 868$ from [AKS14, Table 2], proved by an explicit good partition sorry line 308 source
Source documentation
$W(3, 29) \ge 868$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_29_lower : answer(True) ↔ W 3 29 ≥ 868 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_29_eq [AKS14, Table 2] conjectures that $W(3, 29) = 868$ sorry line 313 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 29) = 868$. This is false: Chowdhury, Codel, and Heule [CCH23, Section 6.3] found a good partition of $\{1, \ldots, 868\}$, so $W(3, 29) \geq 869$.

depends on sorry what this means
Statement uses: Iff, False, Eq, Nat, Green14.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.
```
theorem W_3_29_eq : answer(False) ↔ W 3 29 = 868 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_30_lower $W(3, 30) \ge 903$ from [AKS14, Table 2], proved by an explicit good partition sorry line 317 source
Source documentation
$W(3, 30) \ge 903$ from [AKS14, Table 2], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GE.ge, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_30_lower : answer(True) ↔ W 3 30 ≥ 903 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_30_eq [AKS14, Table 2] conjectures that $W(3, 30) = 903$ sorry line 322 source
Source documentation
[AKS14, Table 2] conjectures that $W(3, 30) = 903$. This is false: Chowdhury, Codel, and Heule [CCH23, Section 6.3] found a good partition of $\{1, \ldots, 903\}$, so $W(3, 30) \geq 904$.

depends on sorry what this means
Statement uses: Iff, False, Eq, Nat, Green14.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.
```
theorem W_3_30_eq : answer(False) ↔ W 3 30 = 903 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_31_lower $W(3, 31) > 930$ from [AKS14, Table 3], proved by an explicit good partition sorry line 328 source
Source documentation
$W(3, 31) > 930$ from [AKS14, Table 3], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GT.gt, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_31_lower : answer(True) ↔ W 3 31 > 930 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_32_lower $W(3, 32) > 1006$ from [AKS14, Table 3], proved by an explicit good partition sorry line 332 source
Source documentation
$W(3, 32) > 1006$ from [AKS14, Table 3], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GT.gt, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_32_lower : answer(True) ↔ W 3 32 > 1006 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_33_lower $W(3, 33) > 1063$ from [AKS14, Table 3], proved by an explicit good partition sorry line 336 source
Source documentation
$W(3, 33) > 1063$ from [AKS14, Table 3], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GT.gt, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_33_lower : answer(True) ↔ W 3 33 > 1063 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_34_lower $W(3, 34) > 1143$ from [AKS14, Table 3], proved by an explicit good partition sorry line 340 source
Source documentation
$W(3, 34) > 1143$ from [AKS14, Table 3], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GT.gt, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_34_lower : answer(True) ↔ W 3 34 > 1143 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_35_lower $W(3, 35) > 1204$ from [AKS14, Table 3], proved by an explicit good partition sorry line 344 source
Source documentation
$W(3, 35) > 1204$ from [AKS14, Table 3], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GT.gt, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_35_lower : answer(True) ↔ W 3 35 > 1204 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_36_lower $W(3, 36) > 1257$ from [AKS14, Table 3], proved by an explicit good partition sorry line 348 source
Source documentation
$W(3, 36) > 1257$ from [AKS14, Table 3], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GT.gt, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_36_lower : answer(True) ↔ W 3 36 > 1257 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_37_lower $W(3, 37) > 1338$ from [AKS14, Table 3], proved by an explicit good partition sorry line 352 source
Source documentation
$W(3, 37) > 1338$ from [AKS14, Table 3], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GT.gt, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_37_lower : answer(True) ↔ W 3 37 > 1338 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_38_lower $W(3, 38) > 1378$ from [AKS14, Table 3], proved by an explicit good partition sorry line 356 source
Source documentation
$W(3, 38) > 1378$ from [AKS14, Table 3], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GT.gt, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_38_lower : answer(True) ↔ W 3 38 > 1378 := sorry
…
```
Mentions: Green14.W
theorem Green14.W_3_39_lower $W(3, 39) > 1418$ from [AKS14, Table 3], proved by an explicit good partition sorry line 360 source
Source documentation
$W(3, 39) > 1418$ from [AKS14, Table 3], proved by an explicit good partition.

depends on sorry what this means
Statement uses: Iff, True, GT.gt, Nat, Green14.W, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
theorem W_3_39_lower : answer(True) ↔ W 3 39 > 1418 := sorry
…
```
Mentions: Green14.W