Back to Problems
erdos_398
Specification
**Brocard's Problem** Does $n! + 1 = m^2$ have integer solutions other than $n = 4, 5, 7$?
Lean 4 Statement
theorem erdos_398 : answer(sorry) ↔ {n | ∃ m, n ! + 1 = m ^ 2} = {4, 5, 7}
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.