Erdős Problem #390: the second-order constant for $f(n)-2n$

Erdős problem #390 · erdosproblems.com/390

Let $f(n)$ be the least $m$ for which $n!$ can be written as $a_1\cdots a_k$ with $n < a_1 < \cdots < a_k = m$ - the smallest possible largest factor in a factorization of $n!$ into distinct integers all exceeding $n$ . Erdős, Guy and Selfridge proved $f(n) - 2n \asymp n/\log n$ . Erdős asked whether there is a constant $c$ with $f(n) - 2n \sim c\,\frac{n}{\log n},$ and what it is.

This preprint answers yes and names the constant: $\lim_{n\to\infty}\frac{(f(n)-2n)\log n}{n} = \frac{4029639598}{25970038185} \approx 0.15516.$

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Argument
Field: factorials
Posed by: Paul Erdos
Year posed: 1980
Years open: 46y
Solved: 2026-07-19
Model: ChatGPT 5.6
Vendor: OpenAI
Collaborators: Shouqiao Wang
Verification: Lean-verified
Publication: Announced
Significance: 13 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

The headline is the constant, and its two halves have different histories. The lower bound, $\liminf (f(n)-2n)/(n/\log n) \ge 4029639598/25970038185$ , is not new here: it is Mausberg's thirteen-layer valuation cut, posted to the erdosproblems.com forum in May 2026 and credited as such in the paper. Its author wrote there that it "does not prove an upper bound, nor does it prove that an asymptotic constant exists."

The novelty is the matching upper bound, so the claim is that the thirteen-layer bound is exactly tight. It is assembled from an exact cofactor-allocation certificate, central-binomial anchors, a guarded rough-signature selector, a friable-number covariance bridge, a finite-band tangent correction, and column-sparse rounding. That construction is what a reader should scrutinize; everything else is inherited or machine-checked.

erdosproblems.com still lists #390 as open, and the paper calls itself a proposed solution.

What the AI did

AI wrote 117 pages proof and wrote 382k lines of Lean 4 code to verify this proof using custom prompt by the author which is also available, prompt does not help AI with any math hints or anything.

Verification

Both halves of the top tier are present, and both were checked here rather than taken on trust.

Statement fidelity: the repository ships a bridge module holding a namespaced copy of the Formal Conjectures extremal function. Diffed against `FormalConjectures/ErdosProblems/390.lean` upstream, the two definitions are identical up to a bound variable's name, and the bridge's terminal `formalF_rhs` is character-for-character the right-hand side of FC's `erdos_390`, which upstream is still marked open. So the formal statement is the problem as posed, pinned in a community-reviewed repository.

Kernel check: the project's CI run of 28 July 2026 is green at the commit that is still the state of `390/lean` today - the only later commit adds a LICENSE. Reading the log rather than the badge: 8,635 targets, zero `declaration uses 'sorry'` warnings against `warningAsError = true`, a source grep that fails the build on sorry, admit, axiom, opaque, sorryAx or unsafe, and an audit step printing `formalF_rhs depends on axioms: [propext, Classical.choice, Quot.sound]` with the workflow asserting that exact string. The work-in-progress dependency PrimeNumberTheoremAnd reports `MediumPNT` axiom-clean in the same log, and the tree declares no axioms of its own.

What this site did not do is re-run the build: the kernel evidence above is the author's public CI, read at the exact commit. And no human has reviewed the mathematics of the upper bound.

Sources

Submitted by QuietNarwhal605 on 17 Aug 2026

Erdős Problem #390: the second-order constant for f(n)−2nf(n)-2nf(n)−2n

What was actually shown

What the AI did

Verification

Sources

Discussion

Erdős Problem #390: the second-order constant for $f(n)-2n$