The known solutions: $4!+1 = 5^2$ , $5!+1 = 11^2$ , $7!+1 = 71^2$

Proved

Brocard.brown_numbers

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

number-theory

The three known solutions of Brocard's equation $n! + 1 = m^2$ :

4! + 1 = 5^2, \qquad 5! + 1 = 11^2, \qquad 7! + 1 = 71^2,

that is, $25 = 25$ , $121 = 121$ and $5041 = 5041$ .

These are the pairs $(n, m) = (4, 5), (5, 11), (7, 71)$ (Brown numbers). This milestone is the inclusion of the three known pairs in the solution set, one of the two directions of the mission's goal.

Preamble

import Mathlib

Formal statement

namespace Brocard

theorem brown_numbers :
    Nat.factorial 4 + 1 = 5 ^ 2 ∧ Nat.factorial 5 + 1 = 11 ^ 2 ∧
      Nat.factorial 7 + 1 = 71 ^ 2 := by sorry

end Brocard

Source

Brocard, Nouv. Corresp. Math. 2 (1876), 287; 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 is a conjunction of three equalities of natural numbers, with no variables and no hypotheses:

4! + 1 = 5^2, \qquad 5! + 1 = 11^2, \qquad 7! + 1 = 71^2.

Numerically these are $24 + 1 = 25$ , $120 + 1 = 121$ and $5040 + 1 = 5041$ . All three must 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

The known solutions: 4!+1=524!+1 = 5^24!+1=52, 5!+1=1125!+1 = 11^25!+1=112, 7!+1=7127!+1 = 71^27!+1=712

The known solutions: $4!+1 = 5^2$ , $5!+1 = 11^2$ , $7!+1 = 71^2$