Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 390

claims/: The 3 claim pages of Problem 390, one per claimant's result; the problem's standing derives from them.

Statement. Let $f(n)$ be the minimal $m$ such that

n! = a_1\cdots a_k

with $n< a_1<\cdots <a_k=m$ . Is there (and what is it) a constant $c$ such that

f(n)-2n \sim c\frac{n}{\log n}?

Status. Claimed, proved. The site labels the problem OPEN (LEAN) and credits no solution. The qualification records Wang's 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 standing derives from the claim pages: the one pending full claim, Wang 2026, is a manuscript found by GPT-5.6 Sol asserting that $f(n)-2n\sim C_0\,n/\log n$ with $C_0=4029639598/25970038185$ , with that Lean development, which this corpus has not built, and no outside reviewer's acceptance; so the problem is claimed, proved. Two partial claims are pending: Erdős, Guy and Selfridge 1982, a proceedings paper proving that $f(n)-2n$ is of exact order $n/\log n$ [EGS82], and Mausberg 2026, a note written with GPT-5.5 Pro proving the lower bound $\liminf(f(n)-2n)\log n/n\ge C_0$ on which the manuscript's lower bound rests.

Source. erdosproblems.com/390, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #390, https://www.erdosproblems.com/390.

References.

[EGS82] Erdős, P. and Guy, R. K. and Selfridge, J. L., Another property of $239$ and some related questions. Congr. Numer. (1982), 243-257.

Formalization. Statement in formal-conjectures; solution at https://github.com/ShouqiaoW/erdos/tree/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (12)

The order of magnitude of f(n) - 2n Mausberg's thirteen-layer lower bound Wang's exact constant for the least top factor problems/factorials_binomials/E0390/claims Factorials and Binomial Coefficients factorials_binomials/alexeev_2025_decomposing_factorial_into_large_factors Theorem 1.3 (pp. 2--3): bounds and asymptotic for t(N), the largest least factor of N! written as N factors factorials_binomials/erdos_1982_another_property_239_related_questions Theorem 3 (p. 244): the least largest factor f(n) of n! into distinct factors above n satisfies 2n + c_1 n/ln n < f(n) < 2n + c_2 n/ln n A Thirteen-Layer Lower Bound for Erdős Problem #390 Theorem 1 (p. 2): liminf (f(n) - 2n)/(n/log n) >= C_0 = 4029639598/25970038185 = 0.15516...factorials_binomials/wang_2026_proposed_solution_erdos_problem_390

Graph