Erdős Problem 373

Reference: erdosproblems.com/373

theorem erdos_373 : S✝.Finite

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.

theorem erdos_373.variants.of_limit (H : Filter.Tendsto (fun (n : ℕ) => ↑(n * (n + 1)).maxPrimeFac / Real.log ↑n) Filter.atTop Filter.atTop) : S✝.Finite

Show that if P(n(n+1)) / log n → ∞ where P(m) denotes the largest prime factor of m, then the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.

theorem erdos_373.variants.of_lower_bound (H : ∀ᶠ (n : ℕ) in Filter.atTop, 4 * Real.log ↑n < ↑(n * (n - 1)).maxPrimeFac) : S✝.Finite

Show that if P(n(n−1)) > 4 log n for large enough n, where P(m) denotes the largest prime factor of m, then the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, has only finitely many solutions.

theorem erdos_373.variants.maximal_solution : (16, [14, 5, 2]) ∈ S✝ ∧ ∀ s ∈ S✝, s.1 ≤ 16

Hickerson conjectured the largest solution the equation n!=a_1!a_2!···a_k!, with n−1 > a_1 ≥ a_2 ≥ ··· ≥ a_k, is 16!=14!5!2!.

theorem erdos_373.variants.suranyi : {(n, a, b) : ℕ × ℕ × ℕ | n.factorial = a.factorial * b.factorial ∧ 1 < n ∧ 1 < a ∧ 1 < b ∧ b ≤ a ∧ a + 1 ≠ n} = {(10, 7, 6)}

Surányi was the first to conjecture that the only non-trivial solution to a!b!=n! is 6!7!=10!.