Erdős Problem 788 — strengthened final theorem

Proved

Erdos788.erdos788

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

combinatoricserdos-problemsextremal-combinatoricsnumber-theory

Let $f(n)$ be the exact integer-valued extremal function in Erdős Problem 788. The complete strengthened theorem asserts all of the following:

\frac1{2000}\sqrt{n\log n}\le f(n) \qquad(n\ge3);

there exist $C>0$ and $n_0\ge1$ such that for every $n\ge n_0$ ,

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

and for every $\varepsilon>0$ , all sufficiently large $n$ satisfy

n^{1/2-\varepsilon}\le f(n)\le n^{1/2+\varepsilon}.

The statement additionally includes, as its own fully quantified conjunct, the affirmative answer to the original Erdős Problems upper-bound question:

\forall\varepsilon>0,\quad f(n)\le n^{1/2+\varepsilon} \quad\text{for all sufficiently large }n.

This is the repository’s strengthened formal version of the public manuscript’s Theorem 1.1: it makes the lower constant explicit and proves that lower bound for every $n\ge3$ .

Preamble

import Definitions.Def_erdos788_problem

Formal statement

namespace Erdos788

/-- Erdős Problem 788, preserving both the strengthened paper statement and
the exact quantifier form of the original upper-bound question. -/
theorem erdos788 : MainTheorem := by sorry

end Erdos788

Source

Shouqiao Wang, Erdős Problem 788 formalization. Final theorem: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/lean/Erdos788/FinalTheorem.lean#L35-L60. Exact target proposition: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/lean/Erdos788/Statement.lean#L44-L59. Reference manuscript: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/paper.pdf, Theorem 1.1; this formal target is the repository's explicitly documented strengthening and also includes the original upper question.

View graph