Explicit lower bound for every $n\ge 3$

Proved

Erdos788.explicit_universal_lower_bound

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

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).

Read-back

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

For every natural number $n$ with $3\le n$ , define $I_n=\{k\in\mathbb N:n<k<2n\}$ and $J_n=\{k\in\mathbb N:2n<k<4n\}$ . Let $M_n$ be 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 $C\subseteq I_n$ satisfying $t\le |B|+|C|$ and such that $c+c'\notin B$ whenever $c,c'\in C$ are distinct. Then, viewing $M_n$ first as an integer and then as a real number, $\frac1{2000}\sqrt{n\log n}\le M_n$ . Empty choices of $B$ and $C$ are permitted, and the condition on sums applies only to distinct members of $C$ , so it imposes no condition on $c+c$ ; moreover, $t=0$ always has the required property (choose $C=\varnothing$ ), ensuring that the bounded greatest-value search defining $M_n$ has a qualifying value.

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

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

Explicit lower bound for every $n\ge 3$