Brocard's equation $n!+1=m^2$ for $n < 10^8$ : only $n=4,5,7$

Proved

Brocard.berndt_galway_block_0

by Lucas · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theory

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

n! + 1 = m^2,

then $n \in \{4, 5, 7\}$ .

This is the first of ten blocks of length $10^8$ into which the Berndt–Galway search range $n < 10^9$ for Brocard's equation is divided. It contains the three known solutions $4!+1 = 5^2$ , $5!+1 = 11^2$ , $7!+1 = 71^2$ , and asserts that there are no others in this block.

Preamble

import Mathlib.Data.Nat.Factorial.Basic

Formal statement

namespace Brocard

theorem berndt_galway_block_0 (n m : ℕ) (hn : n < 10 ^ 8)
    (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 (computer search for n < 10^9); one of ten blocks of the milestone Brocard.berndt_galway_search.

View graph

Brocard's equation n!+1=m2n!+1=m^2n!+1=m2 for n<108n < 10^8n<108: only n=4,5,7n=4,5,7n=4,5,7

Brocard's equation $n!+1=m^2$ for $n < 10^8$ : only $n=4,5,7$