Skip to content

Erdős problem 392

Let A(n)A(n) denote the least value of tt such that n!=a1⋯at n! = a_1 \cdots a_t with a1≤⋯≤at≤n2a_1 \leq \cdots \leq a_t\leq n^2. Then A(n)=n2−n2log⁡n+o(nlog⁡n). A(n) = \frac{n}{2} - \frac{n}{2\log n} + o\left(\frac{n}{\log n}\right).

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/392.lean

Formal Conjectures

FormalConjectures/ErdosProblems/392.leanErdos392.erdos_3924 linesExact file
∀ (A : ℕ → ℕ),  (∀ n > 0,      IsLeast {x | ∃ t, ∃ (_ : ∃ a, n.factorial = ∏ i, a i ∧ Monotone a ∧ a (Fin.last t) ≤ n ^ 2), t + 1 = x} (A n)) →    (fun n => ↑(A n) - ↑n / 2 + ↑n / (2 * Real.log ↑n)) =o[Filter.atTop] fun n => ↑n / Real.log ↑n
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:392
  • PLBY Lean proofsErdosProblems.Erdos392

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page