Back to Problems
erdos_961.jutila_ramachandra_shorey_upper_bound
Specification
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}$.
Lean 4 Statement
theorem erdos_961.jutila_ramachandra_shorey_upper_bound :
(fun k => (f k : ℝ)) =O[atTop] fun k => log (log (log k)) / log (log k) * (k / log k)
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.