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 statement4 of 5

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

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

1∀ (n x : ℕ), n.factorial + 1 ≠ x ^ 4

SolvedStatement only, no proof