Erdős Problem 373

Reference: erdosproblems.com/373

@[reducible, inline]

abbrev Erdos373.S : Set (ℕ × List ℕ)

Let S be the set of non-trivial solutions to the equation n! = a₁! ··· aₖ! such that a₁ ≥ ... ≥ aₖ and n-1 > a₁.

Equations

• Erdos373.S = {(n, l) : ℕ × List ℕ | n.factorial = (List.map Nat.factorial l).prod ∧ List.Sorted (fun (x1 x2 : ℕ) => x1 ≥ x2) l ∧ l.headI < n - 1 ∧ ∀ a ∈ l, 1 < a}

theorem Erdos373.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 Erdos373.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 Erdos373.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 Erdos373.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 Erdos373.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!.