Number theory

Erdős 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.

References

erdosproblems.com/373

No one has attempted this yet.

Formal statement

Lean type

Erdos373.S.Finite

What you must prove

import FormalConjectures.ErdosProblems.«373»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos373.erdos_373" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/373.lean

Source type SHA-256: sha256:62fced4a3e14f77cbd9003cf8673a3aebc0fd436361417c06b9ed720bef0d830
Task id: fc-379fc029-erdos373-erdos-373-bea297d733-formalized-v1
Task commitment: sha256:f61867e2f0f1717691cd1d5f14553713e5a5703598c234bdb635bb633b3fb29a

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.