Theorem 10.3 — Eventual scaled upper bound

Open

Erdos390.eventual_scaled_upper_bound

by ShouqiaoWang · Jul 31, 2026 · Mathlib c5ea003 (Lean v4.30.0)

asymptoticscombinatoricserdos-problemsnumber-theoryupper-bound

Let $f(n)$ be the least possible largest factor in a representation of $n!$ as a product of distinct integers all greater than $n$ , and let

C_0=\frac{4029639598}{25970038185}.

For every real constant $c>C_0$ , all sufficiently large natural numbers $n$ satisfy

f(n)\le 2n+\left\lceil c\frac{n}{\log n}\right\rceil.

This is the paper's eventual upper-bound construction expressed directly as an endpoint estimate.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

/-- The paper's eventual upper endpoint for every constant above `C0`. -/
theorem eventual_scaled_upper_bound :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        f n ≤ 2 * n + Nat.ceil (c * secondOrderScale n) := by sorry

end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdős Problem 390, p. 103, Section 10, Theorem 10.3 (Upper-bound construction), https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex#L10062-L10179. Exact expanded formal endpoint statement: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/BankPaperCanonicalSectionNinePostHeightSourceFirstMainAsymptoticConnectorStatementAudit.lean#L31-L53.

Read-back

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

For every real number $c$ satisfying $\frac{4029639598}{25970038185}<c$ , there exists a natural number $N$ , which may depend on $c$ , such that every natural number $n\ge N$ satisfies the natural-number inequality

f(n)\le 2n+\left\lceil c\,\frac{n}{\log n}\right\rceil_{\mathbb N}.

For $n\ge3$ , $f(n)$ is the least natural number $M$ for which there exists a finite set without repetitions $A\subseteq\{k\in\mathbb N\mid n<k\le M\}$ satisfying $\prod_{a\in A}a=n!$ ; at $n=0,1,2$ , $f(n)=0$ . The real logarithm and real division are totalized: $\log0=\log1=0$ and $x/0=0$ , so $\frac n{\log n}=0$ at $n=0,1$ , while for $n\ge2$ it is the usual positive quotient. The notation $\lceil x\rceil_{\mathbb N}$ denotes natural-number-valued ceiling: for nonnegative $x$ , it is the least natural number $k$ satisfying $x\le k$ , and its totalized extension has value $0$ when $x\le0$ . In this statement, $c$ is positive and $\frac n{\log n}\ge0$ , so its input is nonnegative. The multiplication, addition, and comparison on the right-hand side are all performed in the natural numbers, and the statement imposes no condition on $n<N$ .

Human review

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

View graph