Let $f (n)$ be the minimal $m$ such that $n! = a_{1} \dots a_{k}$ with $n < a_{1} < \dots < a_{k} = m$ . Is there (and what is it) a constant $c$ such that $f (n) - 2 n \sim c \frac{n}{lo g n} ?$

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is still **open** [[nomath]](in particular, the existence of a *limit constant* $c$ is not known)[[/nomath]].

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

AMS 11 · solved (literature)

theorem erdos_390.variants.theta :
    (fun n => f n - 2 * n : ℕ → ℝ) =Θ[atTop] (fun n => n / log (n : ℝ))

open