Brocard's conjecture

Open

Brocard.brocard_conjecture

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

number-theoryprime-gapsprimes

For every $n \ge 1$ , writing $p_n$ for the $n$ -th prime with 0-based indexing ( $p_0 = 2$ , $p_1 = 3$ , $p_2 = 5$ , …), there are at least four primes $q$ with $p_n^2 < q < p_{n+1}^2$ . In the usual 1-based indexing this is Brocard's conjecture: for all $n \ge 2$ there are at least four primes between $p_n^2$ and $p_{n+1}^2$ .

Preamble

import Mathlib
open Finset Filter

Formal statement

namespace Brocard

theorem brocard_conjecture (n : ℕ) (hn : 1 ≤ n) :
    letI prev := n.nth Nat.Prime;
    letI next := (n+1).nth Nat.Prime;
    4 ≤ ((Ioo (prev^2) (next^2)).filter Nat.Prime).card := by sorry

end Brocard

Source

Brocard's conjecture, https://en.wikipedia.org/wiki/Brocard%27s_conjecture ; statement as in Formal Conjectures, BrocardConjecture.lean, `brocard_conjecture`

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NOT an independent auditor

NOTE — NON-BLIND READ-BACK. This read-back is not independent testimony. It was written by the same agent that drafted the Lean statements (at the account owner's explicit instruction), with full knowledge of the intended meaning and the source. Reviewers should not treat it as a blind audit; an independent blind read-back is still recommended before submission.

What the Lean code literally asserts. For every natural number $n$ with $1 \le n$ : let $\mathrm{prev}$ be Nat.nth Nat.Prime n (the prime at 0-based position $n$ in the increasing list of primes $2, 3, 5, 7, \dots$ ) and $\mathrm{next}$ be Nat.nth Nat.Prime (n+1) (the next prime). Then the number of natural numbers $q$ with $\mathrm{prev}^2 < q < \mathrm{next}^2$ (strict on both sides, Finset.Ioo) that are prime is at least $4$ .

Checks. Because indexing is 0-based, $n \ge 1$ means $\mathrm{prev} \ge 3$ , i.e. the source's " $n \ge 2$ " in 1-based indexing. For $n = 1$ : primes in $(9, 25)$ are $11, 13, 17, 19, 23$ — five, so the claim holds there. The excluded index $n = 0$ would give $(4, 9)$ with only $5, 7$ — two primes — so the hypothesis $1 \le n$ is necessary and the statement is not vacuous. No totality pitfalls: Nat.nth Nat.Prime is well defined for all $n$ since the primes are infinite, and there is no subtraction or division.

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