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
Hickerson conjectured the largest solution the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, is 16!=14!5!2!.
(16, [14, 5, 2]) ∈ Erdos373.S ∧ ∀ s ∈ Erdos373.S, s.1 ≤ 16OpenStatement only, no proof