Berndt–Galway: no new solutions of $n!+1=m^2$ with $n < 10^9$

Proved

Brocard.berndt_galway_search

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theory

Let $n$ and $m$ be natural numbers with $n < 10^9$ . If

n! + 1 = m^2,

then $n = 4$ , $n = 5$ or $n = 7$ .

This records the computer search of Berndt and Galway (2000), which found no solutions of Brocard's equation other than the three known ones below $10^9$ . It is the goal restricted to $n < 10^9$ (on the $n$ -coordinate).

Formalization Note The bound is taken strict ( $n < 10^9$ ), which is the weaker reading of the reported search range.

Preamble

import Mathlib

Formal statement

namespace Brocard

theorem berndt_galway_search (n m : ℕ) (hn : n < 10 ^ 9)
    (h : Nat.factorial n + 1 = m ^ 2) : n = 4 ∨ n = 5 ∨ n = 7 := by sorry

end Brocard

Source

B. C. Berndt and W. F. Galway, On the Brocard–Ramanujan Diophantine equation n! + 1 = m^2, Ramanujan J. 4 (2000), 41–42; Formal Conjectures library (Google DeepMind, Apache-2.0), FormalConjectures/Wikipedia/BrocardProblem.lean (pointing to FormalConjectures/ErdosProblems/398.lean), https://github.com/google-deepmind/formal-conjectures ; https://en.wikipedia.org/wiki/Brocard%27s_problem ; https://www.erdosproblems.com/398

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements of this proposal, with full knowledge of the intended meaning and of the source material. It is not independent testimony and should not be treated as a blind audit; an independent read-back is still recommended before launch.

For all natural numbers $n$ and $m$ : if $n < 10^9$ and

n! + 1 = m^2

(an equation of natural numbers, with $0! = 1$ ), then $n = 4$ or $n = 5$ or $n = 7$ .

The conclusion concerns only $n$ ; nothing is asserted about the value of $m$ . The bound on $n$ is strict ( $n = 10^9$ is not covered). There is no bound on $m$ . The cases $n = 0, 1$ are included (for them $n! + 1 = 2$ is not a square, so the hypothesis cannot hold).

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Berndt–Galway: no new solutions of n!+1=m2n!+1=m^2n!+1=m2 with n<109n < 10^9n<109

Berndt–Galway: no new solutions of $n!+1=m^2$ with $n < 10^9$