ErdosProblems · research open · AMS 11
unsolvedsorry — nobody on it
Erdős Problem 373
Conjecture 373 · Erdős
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.
Formal statement · Lean 4.lean
theorem erdos_373 : S.Finite := by
sorryProof. sorry
Nobody has tried yet.