Erdős Problem 200

Reference: erdosproblems.com/200

noncomputable def Erdos200.longestPrimeArithmeticProgressions (n : ℕ) : ℕ

The length of the longest arithmetic progression of primes in $\{1,\ldots,n\}$.

Equations

• Erdos200.longestPrimeArithmeticProgressions n = sSup {k : ℕ | ∃ s ⊆ Set.Icc 1 n, s.IsAPOfLength ↑k ∧ ∀ m ∈ s, Nat.Prime m}

theorem Erdos200.erdos_200 : ((fun (n : ℕ) => ↑(longestPrimeArithmeticProgressions n)) =o[Filter.atTop] fun (n : ℕ) => Real.log ↑n) ↔ sorry

Does the longest arithmetic progression of primes in $\{1,\ldots,N\}$ have length $o(\log N)$?

theorem Erdos200.erdos_200.variants.upper : ∃ (o : ℕ → ℝ) (_ : o =o[Filter.atTop] 1), ∀ (n : ℕ), ↑(longestPrimeArithmeticProgressions n) ≤ (1 + o n) * Real.log ↑n

It follows from the prime number theorem that such a progression has length $\leq(1+o(1))\log N$.