Erdős problem 200

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/200.lean

Formal Conjectures

FormalConjectures/ErdosProblems/200.leanErdos200.erdos_2001 lineExact file

1sorry ↔ (fun n => ↑(Erdos200.longestPrimeArithmeticProgressions n)) =o[Filter.atTop] fun n => Real.log ↑n

OpenStatement only, no proof