Erdős problem 399
Is it true that there are no solutions to n! = x^k ± y^k with x,y,n ∈ ℕ, x*y > 1, and k > 2?
Sources
FormalConjectures/ErdosProblems/
399.lean
Retained formal statement
Is it true that there are no solutions to n! = x^k ± y^k with x,y,n ∈ ℕ, x*y > 1, and k > 2?
The answer is no: Jonas Barfield found the counterexample 10! = 48^4 - 36^4 (equivalently, 10! + 36^4 = 48^4).
This is discussed in problem D2 of Guy's collection [Gu04].
This was formalized in Lean by Lu using Codex.
False ↔ ¬∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n.factorial = x ^ k + y ^ k ∨ n.factorial + y ^ k = x ^ k)