namespace Erdos390

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

end Erdos390

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.