Erdős Problem 398

References:

• erdosproblems.com/398
• Wikipedia: Brocard's problem

theorem erdos_398 : {n : ℕ | ∃ (m : ℕ), n.factorial + 1 = m ^ 2} = {4, 5, 7} ↔ sorry

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