No solutions of $n!+1=m^2$ with $5\cdot 10^8 \le n < 6\cdot 10^8$

Proved

Brocard.berndt_galway_block_5

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

number-theory

Let $n$ and $m$ be natural numbers with

5 \cdot 10^8 \le n < 6 \cdot 10^8.

Then $n! + 1 \neq m^2$ ; that is, Brocard's equation has no solution with $n$ in this range.

This is block number 5 of the ten blocks of length $10^8$ into which the Berndt–Galway search range $n < 10^9$ is divided.

Preamble

import Mathlib.Data.Nat.Factorial.Basic

Formal statement

namespace Brocard

theorem berndt_galway_block_5 (n m : ℕ) (h1 : 5 * 10 ^ 8 ≤ n) (h2 : n < 6 * 10 ^ 8)
    (h : Nat.factorial n + 1 = m ^ 2) : False := 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

No solutions of n!+1=m2n!+1=m^2n!+1=m2 with 5⋅108≤n<6⋅1085\cdot 10^8 \le n < 6\cdot 10^85⋅108≤n<6⋅108

No solutions of $n!+1=m^2$ with $5\cdot 10^8 \le n < 6\cdot 10^8$