399.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 3 contain sorry, 0 declared as axioms

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

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

theorem Erdos399.erdos_399 Is it true that there are no solutions to `n! line 55 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, Not, Exists, Nat, And, LT.lt, OfNat.ofNat, HMul.hMul, Or, Eq, Nat.factorial, HAdd.hAdd, HPow.hPow
Proof uses: id, Eq.mpr, Eq.trans, false_iff, Exists.intro, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_399 : answer(False) ↔
    ¬ ∃ (n x y k : ℕ), 1 < x * y ∧ 2 < k ∧ (n ! = x ^ k + y ^ k ∨ n ! + y ^ k = x ^ k) := by
…
```
theorem Erdos399.erdos_399.variants.erdos_oblath Erdős and Obláth [ErOb37] proved this is true when $(x,y)=1$ and $k\neq 4$ sorry line 63 source
Source documentation
Erdős and Obláth [ErOb37] proved this is true when $(x,y)=1$ and $k\neq 4$.

depends on sorry what this means
Statement uses: Nat, Nat.Coprime, LT.lt, OfNat.ofNat, HMul.hMul, Ne, And, Nat.factorial, HAdd.hAdd, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
theorem Erdos399.erdos_399.variants.pollack_shapiro Pollack and Shapiro [PoSh73] proved there are no solutions to $n!=x^4-1$ sorry line 70 source
Source documentation
Pollack and Shapiro [PoSh73] proved there are no solutions to $n!=x^4-1$.

depends on sorry what this means
Statement uses: Nat, Ne, HAdd.hAdd, Nat.factorial, OfNat.ofNat, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_399.variants.pollack_shapiro (n x : ℕ) : n ! + 1 ≠ x ^ 4 := by
…
```
theorem Erdos399.erdos_399.variants.cambie 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$ line 78 source
Source documentation
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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Coprime, LT.lt, OfNat.ofNat, HMul.hMul, Ne, Nat.factorial, HAdd.hAdd, HPow.hPow
Proof uses: Eq, GE.ge, Or, False, Nat.lt_or_ge, LE.le, dite, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat and 66 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_399.variants.cambie {n x y : ℕ} :
    x.Coprime y → 1 < x * y → n ! ≠ x ^ 4 + y ^ 4 := by
…
```
theorem Erdos399.erdos_399.variants.sum_two_squares Documented declaration: sum_two_squares sorry line 132 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, HMul.hMul, Eq, Nat.factorial, HAdd.hAdd, HPow.hPow, And, Or
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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) := by
…
```