feat(GreensOpenProblems): 37 (google-deepmind#1736)

Formalizes Ben Green's Open Problem 37: finding the smallest subset of ℕ
that contains, for each d = 1, …, N, an arithmetic progression of length
k with common difference d.

Closes google-deepmind#1593

*References:*
- [Ben Green's Open Problem
37](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.37)
- [Green & Tao, *The primes contain arbitrarily long arithmetic
progressions* (arXiv:math/0404188)](https://arxiv.org/abs/math/0404188)

---------

Co-authored-by: Paul Lezeau <lezeau@google.com>

Author: jdhruv555

FormalConjectures/GreensOpenProblems/37.lean

@@ -0,0 +1,79 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Ben Green's Open Problem 37
+
+What is the smallest subset of `ℕ` containing, for each `d = 1, …, N`,
+an arithmetic progression of length `k` with common difference `d`?
+
+*References:*
+- [Ben Green's Open Problem 37](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.37)
+- [Green & Tao, *The primes contain arbitrarily long arithmetic progressions* (arXiv:math/0404188)](https://arxiv.org/abs/math/0404188)
+-/
+
+namespace Green37
+
+open Set Filter
+open scoped Asymptotics
+
+/-- `A` contains an arithmetic progression of length `k` and common difference `d` for every `d ∈ {1, …, N}`. -/
+def IsAPCover (A : Set ℕ) (N k : ℕ) : Prop := ∀ d, 1 ≤ d ∧ d ≤ N → Set.ContainsAP A k d
+
+/-- The minimum size of a subset of `ℕ` that contains, for each `d = 1, …, N`,
+an arithmetic progression of length `k` with common difference `d`. -/
+noncomputable def m (N k : ℕ) : ℕ :=
+  sInf { m | ∃ A : Finset ℕ, A.card = m ∧ IsAPCover (A : Set ℕ) N k }
+
+/--
+Given a natural number `N`, what is the smallest size of a subset of `ℕ` that contains, for each `d = 1, …, N`,
+an arithmetic progression of length `k` with common difference `d`.
+-/
+@[category research open, AMS 05 11]
+theorem green_37 (N k : ℕ) :
+    IsLeast { m | ∃ A : Finset ℕ, A.card = m ∧ IsAPCover (A : Set ℕ) N k } (answer(sorry)) := by
+  sorry
+
+/--
+Asymptotic version: determine the asymptotic behavior of `m(N, k)` as `N` grows.
+The solver should determine what function `f : ℕ → ℝ` eventually equals `(fun N ↦ (m N k : ℝ))`.
+-/
+@[category research open, AMS 05 11]
+theorem green_37_asymptotic (k : ℕ) :
+    ∀ᶠ N in atTop, (m N k : ℝ) = (answer(sorry) : ℕ → ℝ) N := by
+  sorry
+
+/-- Determine the asymptotic equivalence class (theta) of `m(N, k)`. -/
+@[category research open, AMS 05 11]
+theorem green_37_theta (k : ℕ) :
+    (fun N ↦ (m N k : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) := by
+  sorry
+
+/-- Determine an upper bound (big O) for `m(N, k)`. -/
+@[category research open, AMS 05 11]
+theorem green_37_bigO (k : ℕ) :
+    (fun N ↦ (m N k : ℝ)) =O[atTop] (answer(sorry) : ℕ → ℝ) := by
+  sorry
+
+/-- Determine a strict upper bound (little o) for `m(N, k)`. -/
+@[category research open, AMS 05 11]
+theorem green_37_littleO (k : ℕ) :
+    (fun N ↦ (m N k : ℝ)) =o[atTop] (answer(sorry) : ℕ → ℝ) := by
+  sorry
+
+end Green37

FormalConjecturesForMathlib/Combinatorics/AP/Basic.lean

@@ -228,6 +228,10 @@ theorem Set.IsAPOfLengthFree.maxCard_one (N : ℕ) : maxCard 1 N = N := by
   nth_rw 2 [← maxCard_zero N]
   simp [maxCard, isAPOfLengthFree_one, isAPOfLengthFree_zero]
 
+/-- A set `A` contains an arithmetic progression of length `k` with difference `d`. -/
+def Set.ContainsAP (A : Set α) (k : ℕ) (d : α) : Prop :=
+  ∃ a, ∃ s, s ⊆ A ∧ s.IsAPOfLengthWith (k : ℕ∞) a d
+
 def ContainsMonoAPofLength {κ : Type} [Finite κ] {M : Set α}
     (coloring : M → κ) (k : ℕ) : Prop :=
   ∃ c : κ, ∃ ap : Set M, ((·.1) '' ap).IsAPOfLength k ∧