Motivation

Brocard's problem asks for all natural numbers $n$ such that $n! + 1$ is a perfect square. Henri Brocard raised the question in 1876 and again in 1885, and Srinivasa Ramanujan independently posed it in 1913 in the Journal of the Indian Mathematical Society. Only three solutions are known, and the problem is listed as Erdős problem #398 (erdosproblems.com/398). It is one of the simplest-looking Diophantine equations mixing a multiplicative object (the factorial) with an additive shift, and it is a standard test case for conjectures such as the abc conjecture.

Timeline

• 1876, 1885 — Brocard asks whether $n! + 1 = m^2$ has solutions other than $n = 4, 5, 7$.
• 1913 — Ramanujan poses the same question (Question 469, J. Indian Math. Soc.).
• 1993 — Overholt shows that, conditionally on (a weak form of) the abc conjecture, the equation has only finitely many solutions (Wikipedia summary).
• 2000 — Berndt and Galway report a computer search finding no solutions other than $n = 4, 5, 7$ for $n < 10^9$.
• Later searches — the search bound was extended further (Matson, to $10^{12}$; Epstein and Glickman, to $10^{15}$), again without new solutions.

No unconditional proof of finiteness is known.

Setting

For a natural number $n$, the factorial is $n! = 1 \cdot 2 \cdots n$, with $0! = 1$. A Brown number pair is a pair $(n, m)$ of natural numbers with

$$n! + 1 = m^2 .$$

The three known pairs are $(4, 5)$, $(5, 11)$ and $(7, 71)$, since $25 = 5^2$, $121 = 11^2$ and $5041 = 71^2$.

For the conditional milestone, the radical $\operatorname{rad}(N)$ of a natural number $N$ is the product of the distinct primes dividing $N$. The abc conjecture asserts: for every $\varepsilon > 0$ there is $K_\varepsilon > 0$ such that for all positive integers $a, b, c$ with $\gcd(a, b) = 1$ and $a + b = c$,

$$c < K_\varepsilon \, \operatorname{rad}(abc)^{1+\varepsilon}.$$

Formalization targets

Goal — Brocard's problem

$$\{(n, m) \in \mathbb{N}^2 : n! + 1 = m^2\} = \{(4, 5),\ (5, 11),\ (7, 71)\}.$$

This says both that the three known pairs are solutions and that there are no others.

Milestones

1. Known solutions: $4! + 1 = 5^2$, $5! + 1 = 11^2$, $7! + 1 = 71^2$.
2. Berndt–Galway search bound: if $n < 10^9$ and $n! + 1 = m^2$, then $n \in \{4, 5, 7\}$.
3. Overholt (conditional finiteness): if the abc conjecture holds, then $\{(n, m) : n! + 1 = m^2\}$ is finite.

Significance

A resolution would settle a question open since 1876 and would be one of the rare complete solutions of a factorial Diophantine equation of this kind. The conditional finiteness result is a standard illustration of how the abc conjecture controls equations of the form $n! + A = m^2$.

For the formalization, the known-solutions milestone is a finite computation. The search-bound milestone is a large verified computation; a machine-checked certificate for it would be a reusable artifact. The conditional finiteness milestone formalizes a published argument that assumes the abc conjecture as a hypothesis. The goal itself is an open problem; none of these statements is known to have a machine-checked proof on this platform at the time of drafting.

Difficulty

Congruence obstructions cannot rule out large solutions: for every modulus $M$ and every $n \ge M$ one has $n! \equiv 0 \pmod M$, so $n! + 1 \equiv 1 = 1^2 \pmod M$ is a square modulo $M$. Local arguments alone therefore cannot close the problem. The known finiteness argument depends on the abc conjecture, which is itself unproved in the standard form used here. Computer searches only give lower bounds on any further solution.

Formalization scope

• Numbers are natural numbers (ℕ); $m$ ranges over $\mathbb{N}$, so the sign of $m$ is not an issue. The factorial is Mathlib's Nat.factorial, with $0! = 1$.
• The goal is stated as an equality of sets of ordered pairs in $\mathbb{N} \times \mathbb{N}$, so it cannot be satisfied by proving only one inclusion.
• The radical is defined as the product over the prime factors of $N$ (so $\operatorname{rad}(0) = \operatorname{rad}(1) = 1$; the value at $0$ never enters since $a, b, c > 0$).
• The abc conjecture is a Prop-valued definition used as a hypothesis in the conditional milestone; it is not asserted anywhere. The exponent $1 + \varepsilon$ is a real power.
• Overholt's published result assumes only a weak form of abc; the milestone assumes the standard form, which implies the weak form, so the milestone is a consequence of the published result.
• All declarations live in the namespace Brocard.

Selected references

• H. Brocard, Question 166, Nouv. Corresp. Math. 2 (1876), 287; Nouv. Ann. Math. (3) 4 (1885), 391.
• S. Ramanujan, Question 469, J. Indian Math. Soc. 5 (1913), 59.
• M. Overholt, The Diophantine equation $n! + 1 = m^2$, Bull. London Math. Soc. 25 (1993), 104.
• B. C. Berndt and W. F. Galway, On the Brocard–Ramanujan Diophantine equation $n! + 1 = m^2$, Ramanujan J. 4 (2000), 41–42.
• Erdős problem #398: https://www.erdosproblems.com/398
• Brocard's problem, Wikipedia: https://en.wikipedia.org/wiki/Brocard%27s_problem
• Formal Conjectures (Google DeepMind): https://github.com/google-deepmind/formal-conjectures