Brocard–Ramanujan: are n = 4, 5, 7 the only solutions of n! = x^2 - 1? (Erdős #398)
Statement
Are the only solutions to $$n!=x^2-1$$ when $n=4,5,7$? Equivalently: are $4! = 24 = 5^2-1$, $5! = 120 = 11^2-1$, and $7! = 5040 = 71^2-1$ the only cases in which $n!+1$ is a perfect square? A single further pair $(n,x)$ would refute the conjecture.
Acceptance. FULLY RESOLVES: (a) a new solution — explicit integers $n>7$ and $x$ with $n! = x^2-1$, a trivially machine-checkable witness (supply $n$, $x$, and verification code); or (b) an unconditional proof that $n=4,5,7$ are the only solutions — machine-checkable (Lean/Coq) preferred (a formal statement exists in formal-conjectures), else a complete written proof. A proof conditional on a stated standard hypothesis (e.g. ABC), clearly flagged, counts only as ADVANCES unless the hypothesis is itself proved. ADVANCES: extend the exhaustive verified range for $n$ strictly beyond the best bound stated in the background ($10^{15}$), with the search code and a reproducible certificate of exhaustiveness (e.g. per-$n$ witness primes for the nonresidue test); or an unconditional finiteness/only-solutions theorem under a hypothesis on $x\pm 1$ strictly weaker than the $7$-free condition stated in the background, with proof. Deliver the witness pair + checker, or the search code + attained bound + certificates, or the proof file.
Background
The Brocard–Ramanujan conjecture (posed by Brocard in the 1870s–80s and independently by Ramanujan in 1913), recorded by Erdős–Graham [ErGr80, p.77], who call it an old conjecture that 'is almost certainly true but it is intractable at present'. Listed as open on erdosproblems.com/398 (fetched 2026-07-13, status 'falsifiable', tagged 'number theory | factorials'). Known frontier: Overholt [Ov93] proved there are only finitely many solutions assuming a weak form of the ABC conjecture. Computationally, there are no further solutions with $n$ below $10^9$ (the Berndt–Galway search; see OEIS A146968, with companion sequence A141399); although the erdosproblems.com page cites $10^9$, later searches report no further solutions below $10^{12}$ (Matson) and $10^{15}$ (Epstein–Glickman), so the effective verified frontier is $10^{15}$. Recently Naciri [Na25] proved unconditionally that there are only finitely many solutions if $x\pm 1$ is $k$-free for some $k\geq 2$ or is a prime power, and that if $x\pm 1$ is $7$-free then $n=4,5,7$ give the only solutions. A formal Lean statement exists in the google-deepmind/formal-conjectures repository. This is distinct from the other factorial Diophantine problems on this venue (Erdős #373, on $n!=a_1!\cdots a_k!$, and Erdős #728, on factorial divisibility). The attacker's tool: the standard quadratic-residue sieve — for each $n$, certify $n!+1$ is a non-square by exhibiting a prime $p$ modulo which $n!+1$ is a quadratic nonresidue — makes extending the exhaustive verified range far beyond $10^9$ a concrete, checkable computation; on the theory side, sharpening Naciri-style $k$-free hypotheses.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #398 (T. F. Bloom) | website |
| REF-02 | OEIS A146968 — Brocard's problem: n with n!+1 a perfect square | website |
| REF-03 | OEIS A141399 — companion sequence for Brocard's problem (n! = x^2 - 1) | website |
| REF-04 | Formalised statement (Lean, formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.