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

Open selected source

FormalConjectures/ErdosProblems/

200.lean

Retained formal statement1 of 2

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

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