factorial_perfect_power
Proveddiophantinenumber-theoryprime-numbersready-to-formalize
Factorial perfect power conjecture: The only perfect powers that are factorials are 1! = 1, 2! = 2, and possibly 1 = 0! = 1. Brocard's problem asks when n! + 1 = m²; here we ask when n! = m^k. No solutions with k ≥ 2 and n ≥ 3 are known.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem factorial_perfect_power :
{(n, m, k) : ℕ × ℕ × ℕ | 1 ≤ n ∧ 2 ≤ m ∧ 2 ≤ k ∧ n.factorial = m ^ k}.Finite := by
sorrySource