Skip to content

Erdős problem 961

Start work

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

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

961.lean

Retained formal statement4 of 6

Jutila [Ju74], and Ramachandra--Shorey [RaSh73] proved a stronger upper bound f(k)≪log⁡log⁡log⁡klog⁡log⁡kklog⁡kf(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
(fun k => ↑(Erdos961.f k)) =O[Filter.atTop] fun k =>  Real.log (Real.log (Real.log ↑k)) / Real.log (Real.log ↑k) * (↑k / Real.log ↑k)
SolvedStatement only, no proof