Theorem 1.1 — Exact second-order asymptotic

Open

Erdos390.erdos390

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

asymptoticscombinatoricserdos-problemsfactorialsnumber-theory

For every natural number $n\ge3$ , let $f(n)$ be the least possible value of the largest factor in a factorization

n!=a_1a_2\cdots a_k,\qquad n<a_1<a_2<\cdots<a_k.

Let

C_0=\frac{4029639598}{25970038185}.

The theorem asserts the exact second-order asymptotic

f(n)=2n+C_0\frac{n}{\log n} +o\!\left(\frac{n}{\log n}\right) \qquad(n\to\infty).

Equivalently,

\lim_{n\to\infty} \frac{(f(n)-2n)\log n}{n}=C_0.

This determines the asymptotic constant in the second-order term of Erdős Problem 390.

Formalization Note The Lean goal is literally the displayed small- $o$ assertion. The equivalent normalized limit is not added as a separate conjunct. Lean sets $f(n)=0$ for $n<3$ only to make it total; those values do not affect the limit.

Preamble

import Definitions.Def_erdos390_problem

Formal statement

namespace Erdos390

/-- Erdős Problem 390: the exact second-order asymptotic. -/
theorem erdos390 : MainAsymptotic := by sorry

end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdős Problem 390, p. 3, Section 1, Theorem 1.1, https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex#L191-L202. Closed Lean terminal: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/BankPaperCanonicalSectionNinePostHeightSourceFirstMainAsymptoticConnector.lean#L25-L38. Literal expanded audit: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/BankPaperCanonicalSectionNinePostHeightSourceFirstMainAsymptoticConnectorStatementAudit.lean#L55-L64.

Read-back

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

Define $f(n)=0$ when $n=0,1,2$ , and, when $n\ge3$ , define $f(n)$ to be 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 the natural-number product equation $\prod_{a\in A}a=n!$ . The theorem asserts that the function

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

is little- $o$ , along the natural numbers tending to infinity, of the function $n\mapsto\frac n{\log n}$ . Fully expanded, this says that for every real number $\delta>0$ , there exists a natural number $N$ , which may depend on $\delta$ , such that every $n\ge N$ satisfies

\left|f(n)-\left(2n+\frac{4029639598}{25970038185}\frac n{\log n}\right)\right|\le\delta\left|\frac n{\log n}\right|,

with $f(n)$ embedded into the real numbers wherever it occurs. The real denominator in the constant is nonzero. The real logarithm and real division are totalized: in particular, $\log0=\log1=0$ and $x/0=0$ , so the scale $\frac n{\log n}$ is $0$ at $n=0,1$ and is the usual positive quotient for $n\ge2$ . The asymptotic quantifiers allow a different threshold $N$ for each $\delta$ , and impose no requirement on the finite initial segment $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