Eventual quantitative upper bound

Proved

Erdos788.quantitative_upper_bound

by ShouqiaoWang · Jul 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemsextractorstheoretical-computer-scienceupper-bound

There exist an absolute real constant $C>0$ and a natural threshold $n_0\ge1$ such that every natural number $n\ge n_0$ satisfies

f(n)\le n^{\,\frac12+ C\left(\frac{\log\log n}{\log n}\right)^{1/3}}.

This is the eventual quantitative upper-bound component of the strengthened Erdős 788 theorem.

Preamble

import Definitions.Def_erdos788_problem

Formal statement

namespace Erdos788

/-- The quantitative upper bound holds for every sufficiently large natural
number, with an absolute positive exponent constant. -/
theorem quantitative_upper_bound :
    ∃ C : ℝ, 0 < C ∧
      ∃ n₀ : ℕ, 1 ≤ n₀ ∧ ∀ n : ℕ, n₀ ≤ n →
        (f n : ℝ) ≤
          (n : ℝ) ^ ((1 / 2 : ℝ) + C * exponentCorrection n) := by sorry

end Erdos788

Source

Shouqiao Wang, Erdős Problem 788 formalization, UpperFinal.lean, lines 44–59: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/lean/Erdos788/UpperFinal.lean#L44-L59. Reference manuscript: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/paper.pdf, Theorem 1.1.

View graph