Erdős problem 961 · problems.science

It is conjectured that $f(k) \ll (\log k)^O(1)$ .

Sources

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

6 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

961.lean

Retained formal statement4 of 6

Jutila [Ju74], and Ramachandra--Shorey [RaSh73] proved a stronger upper bound $f(k) \ll \frac{\log \log \log k}{\log \log k} \frac{k}{\log k}$ .

FormalConjectures/ErdosProblems/961.leanErdos961.erdos_961.variants.jutila_ramachandra_shorey_upper_bound2 linesExact file

1(fun k => ↑(Erdos961.f k)) =O[Filter.atTop] fun k =>2  Real.log (Real.log (Real.log ↑k)) / Real.log (Real.log ↑k) * (↑k / Real.log ↑k)

SolvedStatement only, no proof