Theorem 1.1 — Exact second-order asymptotic

Open

Erdos390.erdos390

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

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.

View graph