Green_Tao_Theorem
Provedadditive-combinatoricsarithmetic-progressionsgreen-taonumber-theoryprime-numbers
Green–Tao theorem. The primes contain arbitrarily long arithmetic progressions: for every there is a set of primes that forms an arithmetic progression of cardinality at least . (Proved by Green and Tao, 2004; statement following the DeepMind formal-conjectures library, Erdős problem 219.)
Preamble
import Mathlib
def IsAPOfLengthWithDM (s : Set ℕ) (l : ℕ∞) (a d : ℕ) : Prop :=
ENat.card s = l ∧ s = {a + n • d | (n : ℕ) (_ : (n : ℕ∞) < l)}
def IsAPOfLengthDM (s : Set ℕ) (l : ℕ∞) : Prop := ∃ a d : ℕ, IsAPOfLengthWithDM s l a d
def primeArithmeticProgressionsDM : Set (Set ℕ) :=
{s | (∀ p ∈ s, p.Prime) ∧ ∃ l > (0 : ℕ∞), IsAPOfLengthDM s l}Formal statement
theorem Green_Tao_Theorem :
∀ N : ℕ, ∃ s ∈ primeArithmeticProgressionsDM, (N : ℕ∞) ≤ ENat.card s := by sorrySource