Eventual quantitative upper bound

Proved

Erdos788.quantitative_upper_bound

by ShouqiaoWang · 1 vote · Jul 30, 2026 · Mathlib c5ea003 (Lean v4.30.0)

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.

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

There exists a real constant $C>0$ and a natural number $n_0\ge 1$ such that, for every natural number $n\ge n_0$ ,

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

Here $f(n)$ , viewed as a real number in the displayed inequality, is the nonnegative integer obtained as follows: let $I_n=\{m\in\mathbb N:n<m<2n\}$ and $J_n=\{m\in\mathbb N:2n<m<4n\}$ ; then $f(n)$ is the greatest natural number $t\le |J_n|+|I_n|$ such that, for every finite set $B\subseteq J_n$ , there exists a finite set $A\subseteq I_n$ for which no sum $a+a'$ of two distinct members $a,a'\in A$ belongs to $B$ , and $t\le |B|+|A|$ . The quantified $n$ are all positive because $n_0\ge1$ , but $n_0$ itself is allowed to equal $1$ ; consequently the formula does not separately exclude small positive values such as $n=1$ or $n=2$ , and its logarithms, division, cube-root exponentiation, and real powers have the total meanings supplied by the formal real-number operations.

Human review

Endorsed by Shuze Chen · Jul 30, 2026
Endorsed by ShouqiaoWang · Jul 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph