FormalConjectures/Wikipedia/BrocardProblem.lean

GitHub source file

0 declarations, 0 contain sorry, 0 declared as axioms

Brocard's Problem

Brocard's problem asks whether the only solutions to $n! + 1 = m^2$ are $n = 4, 5, 7$.

Reference: Wikipedia

This file points to the canonical formalization in FormalConjectures.ErdosProblems.«398».

Imports (2)

No declarations listed.