For any $k \geq 2$ let $g_{k} (n)$ denote the maximum value of $(a_{1} + \dots + a_{k}) - n$ where $a_{1}, \dots, a_{k}$ are integers such that $a_{1}! \dots a_{k}! ∣ n!$ . Can one show that $n \leq x \sum g_{k} (n) \sim c_{k} x lo g x$ for some constant $c_{k}$ ? Is it true that there is a constant $c_{k}$ such that for almost all $n < x$ we have $g_{k} (n) = c_{k} lo g x + o (lo g x)?$

Worked, still open.

number theory · open · possible · 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 question is (essentially verbatim) **Erdős–Graham problem #400**. As far as I can tell from the standard references, **the specific asymptotics you ask for are still open**, even for (k=2). ([Erdős Problems][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

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

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_400.parts.i :
    answer(sorry) ↔ ∀ᵉ (k ≥ 2), ∃ c : ℝ,
      (fun x : ℕ ↦ (∑ n ∈ Icc 1 x, (g k n : ℝ))) ~[atTop]
      (fun x : ℕ ↦ c * x * Real.log x)

formal-conjectures/400.lean ↗

status

open

evidence

formal

status

Search Vela