Back to Problems
erdos_912.variants.selfridge
Specification
Erdős and Selfridge prove in [Er82c] that $h(n) \asymp \left(\frac{n}{\log n}\right)^{1/2}$.
Lean 4 Statement
theorem erdos_912.variants.selfridge :
(fun n => (h n : ℝ)) =Θ[atTop] (fun n => (n / Real.log n) ^ (1 / 2 : ℝ))
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.