Number theory · Last catalog review 26 Jul 2026

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.

References

erdosproblems.com/373

Published 3 Jun 2026Never attempted

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-e923379e-erdos373-erdos-373-8e122b6ed5-formalized-v1
Task commitment: sha256:24488c677ba9a37a08786d6c5545b675dd15a25cf397d927b7cf063df5ff869c

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.