Erdős problem 200

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

200.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/200.leanErdos200.erdos_200.variants.upper1 lineExact file

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

SolvedStatement only, no proof