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
Surányi was the first to conjecture that the only non-trivial solution to a!b!=n! is 6!7!=10!.
{(n, a, b) | n.factorial = a.factorial * b.factorial ∧ 1 < n ∧ 1 < a ∧ 1 < b ∧ b ≤ a ∧ a + 1 ≠ n} = {(10, 7, 6)}OpenStatement only, no proof