Explicit lower bound for every $n\ge 3$

Proved

Erdos788.explicit_universal_lower_bound

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

combinatoricserdos-problemslower-boundnumber-theory

For every natural number $n\ge3$ , the Erdős 788 extremal function satisfies the explicit lower bound

\frac1{2000}\sqrt{n\log n}\le f(n).

This is the strengthened formal version of the manuscript’s universal lower-bound component: it fixes an absolute constant and makes the estimate valid for every $n\ge3$ , rather than only asymptotically.

Preamble

import Definitions.Def_erdos788_problem

Formal statement

namespace Erdos788

/-- The strengthened explicit lower bound, valid for every `n ≥ 3`. -/
theorem explicit_universal_lower_bound :
    ∀ n : ℕ, 3 ≤ n →
      finalLowerBoundConstant *
          Real.sqrt ((n : ℝ) * Real.log (n : ℝ)) ≤
        (f n : ℝ) := by sorry

end Erdos788

Source

Shouqiao Wang, Erdős Problem 788 formalization, LowerFinal.lean, lines 348–353: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/lean/Erdos788/LowerFinal.lean#L348-L353. This is the repository's explicit strengthening of the manuscript's Proposition 3.4 (https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/paper.pdf).

View graph

Explicit lower bound for every n≥3n\ge 3n≥3

Explicit lower bound for every $n\ge 3$