Back to Problems
erdos_1085_lower_d3
Specification
Erdős showed $f_3(n) = Ω(n^{4/3}\log\log n)$.
Lean 4 Statement
theorem erdos_1085_lower_d3 :
(fun n : ℕ ↦ (n : ℝ) ^ (4/3 : ℝ) * log (log n)) =O[atTop] (fun n ↦ (f 3 n : ℝ))
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.