Erdős problem 392

Let $A(n)$ denote the least value of $t$ such that $n! = a_1 \cdots a_t$ with $a_1 \leq \cdots \leq a_t\leq n^2$ . Then $A(n) = \frac{n}{2} - \frac{n}{2\log n} + o\left(\frac{n}{\log n}\right).$

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

392.lean

Retained formal statement3 of 3

If we change the condition to $a_t \leq n$ it can be shown that $A(n) = n - \frac{n}{\log n} + o\left(\frac{n}{\log n}\right)$

FormalConjectures/ErdosProblems/392.leanErdos392.erdos_392.variants.lower3 linesExact file

1∀ (A : ℕ → ℕ),2  (∀ n > 0, IsLeast {x | ∃ t, ∃ (_ : ∃ a, n.factorial = ∏ i, a i ∧ Monotone a ∧ a (Fin.last t) ≤ n), t + 1 = x} (A n)) →3    (fun n => ↑(A n) - ↑n + ↑n / Real.log ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n

SolvedStatement only, no proof