The board / number theory / #373
Erdős Problem #373
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Let `S` be the set of non-trivial solutions to the equation `n! = a₁! ··· aₖ!` such that `a₁ ≥ ... ≥ aₖ` and `n-1 > a₁`.
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.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/373.Prizenone
Topicsnumber theory, factorials
Statement in LeanFormal Conjectures
Solution in Leanno
OEISA003135
Original pageerdosproblems.com/373
Attempts
submit one →Read our working report →
The problem remains open; primary literature gives the omitted unconditional Hickerson classification through \(n\le e^{80}\), while an exact valuation recursion independently finds only the four know
PARTIAL