Brocard's problem: $n! + 1 = m^2$ exactly for $(n,m) = (4,5), (5,11), (7,71)$

Open

Brocard.brocard_problem

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

number-theory

Brocard's problem. The pairs $(n, m)$ of natural numbers satisfying

n! + 1 = m^2

are exactly $(4, 5)$ , $(5, 11)$ and $(7, 71)$ . Equivalently: $n! + 1$ is a perfect square if and only if $n \in \{4, 5, 7\}$ , and in those cases $n! + 1$ equals $5^2 = 25$ , $11^2 = 121$ and $71^2 = 5041$ respectively.

This is the Brocard–Ramanujan problem (Erdős problem #398), open since 1876. Pairs with $n! + 1 = m^2$ are called Brown numbers.

Formalization Note The statement is an equality of sets of ordered pairs in $\mathbb{N} \times \mathbb{N}$ ; $m$ ranges over natural numbers, and $0! = 1$ .

Preamble

import Mathlib

Formal statement

namespace Brocard

theorem brocard_problem :
    {p : ℕ × ℕ | Nat.factorial p.1 + 1 = p.2 ^ 2} = {(4, 5), (5, 11), (7, 71)} := by sorry

end Brocard

Source

Brocard's problem / Brocard–Ramanujan equation; Erdős problem #398. 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.

The statement asserts an equality of two sets of ordered pairs of natural numbers (natural numbers include $0$ ). The left-hand set is

S = \{(n, m) \in \mathbb{N} \times \mathbb{N} \;:\; n! + 1 = m^2\},

where $n!$ is the usual factorial with $0! = 1$ , and the equation is an equation of natural numbers. The right-hand set is the three-element set $\{(4, 5), (5, 11), (7, 71)\}$ .

The equality therefore claims both:

each of $(4,5)$ , $(5,11)$ , $(7,71)$ satisfies $n! + 1 = m^2$ (that is, $25 = 5^2$ , $121 = 11^2$ , $5041 = 71^2$ ); and
every pair of natural numbers $(n, m)$ with $n! + 1 = m^2$ is one of these three pairs.

The quantification includes $n = 0$ and $n = 1$ (where $n! + 1 = 2$ , not a square) and $m = 0$ . Negative $m$ are not considered, since $m$ is a natural number. There are no hypotheses.

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

Brocard's problem: n!+1=m2n! + 1 = m^2n!+1=m2 exactly for (n,m)=(4,5),(5,11),(7,71)(n,m) = (4,5), (5,11), (7,71)(n,m)=(4,5),(5,11),(7,71)

Brocard's problem: $n! + 1 = m^2$ exactly for $(n,m) = (4,5), (5,11), (7,71)$