---

Claim. Shouqiao Wang's manuscript "A Proposed Solution to Erdős Problem 390" (in the author's GitHub repository, uploaded 2026-07-18 and revised on 2026-07-19 and 2026-07-22; the link pins the revision of 2026-07-28 that added the Lean development) answers the question of Problem 390 yes, with an explicit constant. For $f(n)$ the least $m$ such that $n!=a_1\cdots a_k$ with $n<a_1<\cdots<a_k=m$, its Theorem 1.1 states

$$f(n)=2n+C_0\frac{n}{\log n}+o\Bigl(\frac{n}{\log n}\Bigr),\qquad C_0=\frac{4029639598}{25970038185}=0.15516\ldots$$

The lower bound $\liminf_n(f(n)-2n)\log n/n\ge C_0$ is a thirteen-layer valuation obstruction. In the complement form, $f(n)\le M$ holds exactly when $M!/(n!)^2$ is a product of distinct integers in $(n,M]$; a first lemma rules out every $M\le2n$, and for $M>2n$ the primes $P$ in the thirteen layers $M/(2r+2)<P\le M/(2r+1)$ with $n/(r+1)<P\le n/r$, $1\le r\le13$, divide that quotient exactly once and force factors whose cofactors carry a prime at most $23$, and comparing the valuations so forced with those available gives $C_0$ as the ratio of $\sum_{r=1}^{13}1/((r+1)(2r+1))$ to $\sum_{p\le23}1/(p-1)$. The manuscript's section 3 says that this argument is the one of Mausberg's note of 2026-05-02, written with GPT-5.5 Pro, which has its own claim page, Mausberg 2026; Erdős, Guy and Selfridge had shown that $f(n)-2n$ is of exact order $n/\log n$ ([EGS82], carded at Erdős, Guy and Selfridge 1982). The upper bound, the manuscript's Theorem 10.3, is the new part: for every $c>C_0$ and all large $n$ it builds a factorization whose largest factor is at most $2n+cn/\log n$, assigning the large prime factors explicitly, finding a fractional allocation of the small-prime exponents from the supply of smooth numbers with a Poisson–Dickman model of their distribution, and turning it into distinct integers by local swaps and a final rounding-and-switching step; a companion Python script is said to check the finite allocation certificate. The digest is on the library card Wang 2026.

Submission note. Posted to erdosproblems.com as a proof claim by Shouqiao Wang (account ShouqiaoWang) on 19 July 2026, giving "GPT-5.6 Sol" as the AI used:

We claims that

$$> f(n)=2n+\frac{4029639598}{25970038185}\frac{n}{\log n}+o\left(\frac n{\log n}\right). >$$

The lower bound is essentially the thirteen-layer obstruction already posted in the comments. The upper bound is the new part. After taking complements, the task is to build the exact quotient $M!/(n!)^2$ from distinct numbers between $n$ and $M$. The large prime factors can be assigned fairly explicitly. The main difficulty is making all the smaller prime exponents come out right at the same time. The proof uses the supply of smooth numbers to find a fractional solution, with the Poisson–Dickman model showing that there is enough freedom to make the required adjustments. A few local swaps fix the remaining errors, and a final rounding-and-switching step turns this into an exact set of distinct integers. Notes: This proof was found by GPT-5.6 Sol through my AI pipeline. It is quite long and complicated, but I have tried my best to understand the overall argument, and the main ideas seem to make sense to me. It has also gone through several rounds of AI checking, including checking the lemmas and propositions one by one. I am currently generating a Lean formalization and will submit it once that is ready.

Depends on. Mausberg 2026 supplies the lower bound: the manuscript's section 3 states that its lower-bound argument is Mausberg's thirteen-layer obstruction, with a preliminary lemma that rules out endpoints at or below $2n$. That claim is pending, so the dependency raises no standing.

Formalization. The repository's folder 390/lean, added on 2026-07-28 and announced by the author in the claim's comments on 2026-07-29, is a Lean 4 development of 1,846 Lean files. Its terminal theorem bankPaperCanonicalSectionNinePostHeight_sourceFirstMainAsymptotic proves a proposition MainAsymptotic declared with no hypotheses, and a bridge module restates the extremal function in the form the formal-conjectures statement file uses, proves that the two agree for $n\ge3$, and derives from the main theorem both $f(n)-2n=\Theta(n/\log n)$ and $f(n)-2n\sim C_0n/\log n$. The audit file prints the axioms of these declarations and asserts them free of sorry; it also says that five theorems of an earlier conditional skeleton take analytic estimates as hypotheses, which the axiom printout does not reveal, and that it is not an audit of the paper's Lemmas 7.5, 8.4 and 8.6 or Proposition 8.7. This corpus has not built or audited the development, so the link is a formalization link and gives no formalized evidence.

Authorship and tools. The claim's notes say that GPT-5.6 Sol found the proof through the author's AI pipeline, that the author followed the overall argument and found its main ideas sound, and that the lemmas and propositions went through several rounds of AI checking one by one; the manuscript says the solution was found by GPT-5.6. The submitter is the claimant, and the forum names the system as GPT-5.6 Sol.

Standing. Posted on the problem's proof-claims tab as a full claim on 2026-07-19. Of its two comments, one (2026-07-23) objects that the abstract is unreadable, and the other (2026-07-29) is the author's link to the Lean development. The manuscript is not refereed and no outside reviewer has recorded accepting it. The site labels the problem OPEN (LEAN): the qualification records this Lean development, which the site's community database lists (2026-08-28) as machine-checked against Mathlib and bridged to the formal-conjectures statement, with the informal status left open until a human reader has digested it; the site's remarks do not mention the manuscript. This corpus has not built the development, so the claim stays claimed, and the problem's standing is claimed, proved, through this pending full claim.