feat: add Green-Tao theorem eval problem

LeanEval/NumberTheory/GreenTao.lean

@@ -0,0 +1,34 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace NumberTheory
+
+/-!
+# Green–Tao theorem
+
+§37 of Oliver Knill's *Some Fundamental Theorems in Mathematics*. The set
+of primes contains arbitrarily long arithmetic progressions: for every `k`
+there exist `a ≥ 0` and `b ≥ 1` such that `a + b · j` is prime for every
+`j < k`.
+
+mathlib has Dirichlet's theorem (`Nat.infinite_setOf_prime_and_modEq`) and
+Roth's theorem on 3-APs (`roth_3ap_theorem_nat`) but **not** the
+Green–Tao theorem. As of 2026 it has not been formalized in any major
+proof assistant (a long-standing open formalization target).
+-/
+
+/-- A set `A ⊆ ℕ` contains **arbitrarily long arithmetic progressions** if
+for every length `k` there is an AP `{a + b·j | j < k}` of common
+difference `b ≥ 1` entirely contained in `A`. -/
+def ContainsArbitraryAPs (A : Set ℕ) : Prop :=
+  ∀ k : ℕ, ∃ a b : ℕ, 1 ≤ b ∧ ∀ j : ℕ, j < k → a + b * j ∈ A
+
+/-- **Green–Tao theorem.** The set of primes contains arbitrarily long
+arithmetic progressions. -/
+@[eval_problem]
+theorem green_tao : ContainsArbitraryAPs {p : ℕ | Nat.Prime p} := by
+  sorry
+
+end NumberTheory
+end LeanEval

manifests/problems.toml

@@ -673,3 +673,14 @@ module = "LeanEval.Geometry.Uniformization"
 holes = ["uniformization"]
 submitter = "Junyan Xu"
 source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1."
+
+[[problem]]
+id = "green_tao"
+title = "Green–Tao theorem"
+test = false
+module = "LeanEval.NumberTheory.GreenTao"
+holes = ["green_tao"]
+submitter = "Kim Morrison"
+notes = "§37 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The set of primes contains arbitrarily long arithmetic progressions: for every k there exist a ≥ 0 and b ≥ 1 such that a + b·j is prime for every j < k. Mathlib has Dirichlet's theorem (Nat.infinite_setOf_prime_and_modEq) and Roth's theorem on 3-APs (roth_3ap_theorem_nat) but not Green-Tao. As of 2026 the theorem has not been formalized in any major proof assistant (a long-standing open formalization target)."
+source = "B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Ann. of Math. 167 (2008), 481-547 (announced 2004). Listed as §37 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)."
+informal_solution = "The proof has three main steps. (i) A transference principle: it suffices to find arbitrarily long APs in any set of positive density in a suitable pseudorandom super-set. (ii) Pseudorandomness of the primes after a `W-trick': removing small prime factors via a Selberg-style sieve makes the indicator function of the primes dominated by a pseudorandom measure ν. (iii) Apply Szemerédi's theorem in the relative form (a Furstenberg-style multiple recurrence / Gowers-uniformity argument) to that pseudorandom set, transferring the AP-rich conclusion back to the primes."