Lemma 3.2 — Thirteen-layer lower bound

Proved

Erdos390.eventual_thirteen_layer_lower_bound

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

analytic-number-theoryasymptoticserdos-problemslower-boundnumber-theory

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 $\varepsilon>0$ , all sufficiently large natural numbers $n$ satisfy

2n+(C_0-\varepsilon)\frac{n}{\log n}\le f(n).

Equivalently, the normalized second-order excess of $f(n)$ has lower limit at least $C_0$ . This is the paper's thirteen-layer lower-bound milestone.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

/-- The paper's thirteen-layer lower bound, with all quantifiers explicit. -/
theorem eventual_thirteen_layer_lower_bound :
    ∀ ε : ℝ, 0 < ε →
      ∀ᶠ n : ℕ in atTop,
        2 * (n : ℝ) + (C0 - ε) * secondOrderScale n ≤ (f n : ℝ) := by sorry

end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdős Problem 390, p. 10, Section 3, Lemma 3.2 (Thirteen-layer lower bound), https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex#L847-L984. Exact formal endpoint bound: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/ThirteenLayerLowerBound.lean#L222-L333.

Read-back

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

For every real number $\varepsilon>0$ , there exists a natural number $N$ , which may depend on $\varepsilon$ , such that every natural number $n\ge N$ satisfies the real-number inequality

2n+\left(\frac{4029639598}{25970038185}-\varepsilon\right)\frac{n}{\log n}\le f(n).

On the right-hand side, the natural number $f(n)$ is embedded into the real numbers. For $n\ge3$ , $f(n)$ is the least natural number $M$ for which there exists a finite set $A\subseteq\{k\in\mathbb N\mid n<k\le M\}$ , with distinct elements, satisfying $\prod_{a\in A}a=n!$ ; at $n=0,1,2$ , $f(n)=0$ . The real logarithm and real division are both totalized: $\log0=\log1=0$ and $x/0=0$ , so $\frac0{\log0}=\frac1{\log1}=0$ , while for $n\ge2$ , $\frac n{\log n}$ is the usual positive quotient. The quantifier ranges over every positive $\varepsilon$ , with no upper bound imposed on $\varepsilon$ , and the statement does not require the inequality to hold when $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