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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

399.lean

Retained formal statement3 of 5

Erdős and Obláth [ErOb37] proved this is true when $(x,y)=1$ and $k\neq 4$ .

FormalConjectures/ErdosProblems/399.leanErdos399.erdos_399.variants.erdos_oblath1 lineExact file

1∀ {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

SolvedStatement only, no proof