Skip to content

Erdős problem 219

Start work

Are there arbitrarily long arithmetic progressions of primes? Solution: yes. Ref: Green, Ben and Tao, Terence, _The primes contain arbitrarily long arithmetic progressions_

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

219.lean

Retained formal statement2 of 6

Are there arbitrarily long arithmetic progressions of primes? Solution: yes. Ref: Green, Ben and Tao, Terence, _The primes contain arbitrarily long arithmetic progressions_

FormalConjectures/ErdosProblems/219.leanErdos219.erdos_2191 lineExact file
True ↔ ∀ (N : ℕ), ∃ l ∈ Erdos219.primeArithmeticProgressions, ↑N ≤ ENat.card ↑l
SolvedStatement only, no proof