Erdős Problem 399

Is it true that there are no solutions to $n! = x^k \pm y^k$ with $x,y,n \in \mathbb{N}$, with $xy > 1$ and $k > 2$?

References:

• erdosproblems.com/399
• [Br32] R. Breusch, Zur Verallgemeinerung des Bertrandschen Postulates (1932)
• [ErOb37] P. Erdős and R. Obláth, Über diophantische Gleichungen der Form $n!=x^p+y^p$ und $n!\pm m!=x^p$ (1937)
• [PoSh73] R. Pollack and H. Shapiro, The next to last case of a factorial diophantine equation (1973)
• [Gu04] R. Guy, Unsolved problems in number theory (2004)

theorem Erdos399.erdos_399 : False ↔ ¬∃ (n : ℕ) (x : ℕ) (y : ℕ) (k : ℕ), 1 < x * y ∧ 2 < k ∧ (n.factorial = x ^ k + y ^ k ∨ n.factorial + y ^ k = x ^ k)

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).

theorem Erdos399.erdos_399.variants.erdos_oblath {n x y k : ℕ} : x.Coprime y → 1 < x * y → 2 < k → k ≠ 4 → n.factorial ≠ x ^ k + y ^ k ∧ n.factorial + y ^ k ≠ x ^ k

Erdős and Obláth proved there are no solutions when x.Coprime y and k ≠ 4.

theorem Erdos399.erdos_399.variants.pollack_shapiro (n x : ℕ) : n.factorial + 1 ≠ x ^ 4

Pollack and Shapiro proved there are no solutions to n! = x^4 - 1.

theorem Erdos399.erdos_399.variants.cambie {n x y : ℕ} : x.Coprime y → 1 < x * y → n.factorial ≠ x ^ 4 + y ^ 4

Cambie observed that there are no solutions to n! = x^4 + y^4 with x.Coprime y and x*y > 1.

theorem Erdos399.erdos_399.variants.sum_two_squares {n x y : ℕ} : 1 < x * y → n.factorial = x ^ 2 + y ^ 2 → n = 6 ∧ (x = 12 ∧ y = 24 ∨ x = 24 ∧ y = 12)

The only solution to n! = x^2 + y^2 with x*y > 1 is 6! = 12^2 + 24^2 (up to swapping x and y).