Lemma 3.2 — Thirteen-layer lower bound

Proved

Erdos390.eventual_thirteen_layer_lower_bound

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

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.

View graph