Skip to content

Erdős problem 390

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

390.lean

Retained formal statement1 of 2

Does there exists a constant c such that f n - 2 * n ~ c * (n / log n)?

FormalConjectures/ErdosProblems/390.leanErdos390.erdos_3901 lineExact file
True ↔ ∃ c, Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos390.f n) - 2 * ↑n) fun n => c * ↑n / Real.log ↑n
OpenStatement only, no proof