erdos_160.known_upper

Specification

On [Mathoverflow](https://mathoverflow.net/a/410815) user [leechlattice](https://mathoverflow.net/users/125498/leechlattice) shows that $h(n) \ll n^{\frac 2 3}$.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem erdos_160.known_upper :
    (fun n => (erdos_160.h n : ℝ)) =O[atTop] fun n => (n : ℝ) ^ ((2 : ℝ) / 3)

ID: ErdosProblems__160__erdos_160.known_upper

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.