Erdős problem 200 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

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