Overholt: the abc conjecture implies $n!+1=m^2$ has finitely many solutions

Proved

Brocard.overholt_finite_of_abc

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

number-theory

Assume the abc conjecture: for every $\varepsilon > 0$ there is $K_\varepsilon > 0$ such that $c < K_\varepsilon \operatorname{rad}(abc)^{1+\varepsilon}$ for all positive integers $a, b$ with $\gcd(a,b) = 1$ and $c = a + b$ , where $\operatorname{rad}(N)$ is the product of the distinct primes dividing $N$ . Then the set

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

is finite.

This is Overholt's conditional finiteness theorem for Brocard's equation (1993).

Formalization Note Overholt's argument needs only a weak form of the abc conjecture; the hypothesis here is the standard form (see the definition file Brocard_Defs), which implies the weak form. The abc conjecture is a hypothesis of the theorem, not an assumption of the platform.

Preamble

import Mathlib
import Definitions.Def_Brocard_Defs

Formal statement

namespace Brocard

theorem overholt_finite_of_abc (habc : ABCConjecture) :
    {p : ℕ × ℕ | Nat.factorial p.1 + 1 = p.2 ^ 2}.Finite := by sorry

end Brocard

Source

M. Overholt, The Diophantine equation n! + 1 = m^2, Bull. London Math. Soc. 25 (1993), 104; 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.

Hypothesis: the proposition $\mathrm{ABCConjecture}$ holds, namely: for every real $\varepsilon > 0$ there is a real $K > 0$ such that for all natural numbers $a, b, c$ with $a > 0$ , $b > 0$ , $\gcd(a, b) = 1$ and $a + b = c$ ,

c < K \cdot \operatorname{radical}(abc)^{1+\varepsilon},

where $\operatorname{radical}(N)$ is the product of the distinct primes dividing $N$ (equal to $1$ for $N = 0, 1$ ), and the power is a real power with real exponent.

Conclusion: the set

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

of ordered pairs of natural numbers (with $0! = 1$ ) is a finite set.

The conclusion is finiteness only; no bound on the number or size of solutions is stated, and no specific solutions are named. The theorem does not assert the abc conjecture itself; if the abc conjecture were false, the statement would hold vacuously.

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

Overholt: the abc conjecture implies n!+1=m2n!+1=m^2n!+1=m2 has finitely many solutions

Overholt: the abc conjecture implies $n!+1=m^2$ has finitely many solutions