Erdős problem 398

Brocard's Problem Does $n! + 1 = m^2$ have integer solutions other than $n = 4, 5, 7$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

398.lean

Retained formal statement1 of 1

Brocard's Problem Does $n! + 1 = m^2$ have integer solutions other than $n = 4, 5, 7$ ?

FormalConjectures/ErdosProblems/398.leanErdos398.erdos_3981 lineExact file

1sorry ↔ {n | ∃ m, n.factorial + 1 = m ^ 2} = {4, 5, 7}

OpenStatement only, no proof