/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtilErdő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:
[Br32] Breusch, Robert, Zur Verallgemeinerung des Bertrandschen Postulates, da\ss zwischen $x$ und 2 $x$ stets Primzahlen liegen. Math. Z. (1932), 505--526.
[ErOb37] Erdős, P. and Obláth, R., "Über diophantische Gleichungen der Form $n!=x^p+y^p$ und $n!\pmd m!=x^p$. Acta Litt. ac Sci. Reg. Univ. Hung. Fr.-Jos., Sect. Sci. Math. (1937), 241-255.
[Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
[PoSh73] Pollack, Richard M. and Shapiro, Harold N., The next to last case of a factorial diophantine equation. Comm. Pure Appl. Math. (1973), 313-325.
@[expose] public sectionopen Natnamespace Erdos399
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.
@[category research solved, AMS 11]
theorem erdos_399 : answer(False) ↔
¬ ∃ (n x y k : ℕ), 1 < x * y ∧ 2 < k ∧ (n ! = x ^ k + y ^ k ∨ n ! + y ^ k = x ^ k) := ⊢ False ↔ ¬∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n ! = x ^ k + y ^ k ∨ n ! + y ^ k = x ^ k)
⊢ False ↔ ¬∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n ! = x ^ k + y ^ k ∨ n ! + y ^ k = x ^ k)
⊢ ∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n ! = x ^ k + y ^ k ∨ n ! + y ^ k = x ^ k)
exact ⟨10, 48, 36, 4, ⊢ 1 < 48 * 36 ∧ 2 < 4 ∧ (10! = 48 ^ 4 + 36 ^ 4 ∨ 10! + 36 ^ 4 = 48 ^ 4) All goals completed! 🐙⟩Erdős and Obláth [ErOb37] proved this is true when $(x,y)=1$ and $k\neq 4$.
@[category research solved, AMS 11]
theorem erdos_399.variants.erdos_oblath {n x y k : ℕ} :
x.Coprime y → 1 < x * y → 2 < k → k ≠ 4 →
n ! ≠ x ^ k + y ^ k ∧ n ! + y ^ k ≠ x ^ k := n:ℕx:ℕy:ℕk:ℕ⊢ x.Coprime y → 1 < x * y → 2 < k → k ≠ 4 → n ! ≠ x ^ k + y ^ k ∧ n ! + y ^ k ≠ x ^ k
All goals completed! 🐙Pollack and Shapiro [PoSh73] proved there are no solutions to $n!=x^4-1$.
@[category research solved, AMS 11]
theorem erdos_399.variants.pollack_shapiro (n x : ℕ) : n ! + 1 ≠ x ^ 4 := n:ℕx:ℕ⊢ n ! + 1 ≠ x ^ 4
All goals completed! 🐙Cambie has also observed that considerations modulo $8$ rule out any solutions to $n!=x^4+y^4$ with $(x,y)=1$ and $xy>1$.
n:ℕx:ℕy:ℕhxy:x.Coprime yh1:1 < x * yheq:n ! = x ^ 4 + y ^ 4hn:n ≥ 4h4le:4! ∣ n !h8:8 ∣ n !h8':8 ∣ x ^ 4 + y ^ 4hnotboth2:x % 2 = 1 ∨ y % 2 = 1parity4:∀ (z : ℕ), z ^ 4 % 8 = z % 2⊢ False
n:ℕx:ℕy:ℕhxy:x.Coprime yh1:1 < x * yheq:n ! = x ^ 4 + y ^ 4hn:n ≥ 4h4le:4! ∣ n !h8:8 ∣ n !h8':8 ∣ x ^ 4 + y ^ 4hnotboth2:x % 2 = 1 ∨ y % 2 = 1parity4:∀ (z : ℕ), z ^ 4 % 8 = z % 2hx4:x ^ 4 % 8 = x % 2⊢ False
n:ℕx:ℕy:ℕhxy:x.Coprime yh1:1 < x * yheq:n ! = x ^ 4 + y ^ 4hn:n ≥ 4h4le:4! ∣ n !h8:8 ∣ n !h8':8 ∣ x ^ 4 + y ^ 4hnotboth2:x % 2 = 1 ∨ y % 2 = 1parity4:∀ (z : ℕ), z ^ 4 % 8 = z % 2hx4:x ^ 4 % 8 = x % 2hy4:y ^ 4 % 8 = y % 2⊢ False
All goals completed! 🐙Erdős and Obláth observed that the Bertrand-style fact (first proved by Breusch [Br32]) that, if $q_i$ is the sequence of primes congruent to $3\pmod{4}$ then $q_{i+1}<2q_i$ except for $q_1=3$, together with Fermat's theorem on the sums of two squares implies that the only solution to $n!=x^2+y^2$ is $6!=12^2+24^2$.
@[category research solved, AMS 11]
theorem erdos_399.variants.sum_two_squares :
∀ {n x y : ℕ}, 1 < x * y → n ! = x ^ 2 + y ^ 2 →
n = 6 ∧ (x = 12 ∧ y = 24 ∨ x = 24 ∧ y = 12) := ⊢ ∀ {n x y : ℕ}, 1 < x * y → n ! = x ^ 2 + y ^ 2 → n = 6 ∧ (x = 12 ∧ y = 24 ∨ x = 24 ∧ y = 12)
All goals completed! 🐙end Erdos399