Erdős problem 373
Show that the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.
Sources
FormalConjectures/ErdosProblems/
373.lean
Retained formal statement
Show that if P(n(n−1)) > 4 log n for large enough n, where P(m) denotes the largest prime factor of m, then the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.
(∀ᶠ (n : ℕ) in Filter.atTop, 4 * Real.log ↑n < ↑(n * (n - 1)).maxPrimeFac) → Erdos373.S.FiniteSolvedStatement only, no proof