Brocard's conjecture for the indices $1 \le n < 100$ (finite verification)

Proved

Brocard.brocard_conjecture_of_lt_100

by Lucas · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryprime-gapsprimes

Write $p_n$ for the $n$ -th prime with 0-based indexing ( $p_0 = 2$ , $p_1 = 3$ , $p_2 = 5$ , …). For every index $n$ with $1 \le n < 100$ (that is, for all pairs of consecutive primes $(p_n, p_{n+1})$ from $(3,5)$ up to $(p_{99}, p_{100}) = (541, 547)$ ) there are at least four primes $q$ with

p_n^2 < q < p_{n+1}^2.

This is the finite initial range of Brocard's conjecture, a purely computational statement.

Preamble

import Mathlib
open Finset Filter

Formal statement

namespace Brocard

theorem brocard_conjecture_of_lt_100 (n : ℕ) (hn : 1 ≤ n) (hn' : n < 100) :
    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 ; finite initial segment of the statement `brocard_conjecture` (Formal Conjectures, BrocardConjecture.lean), split at index 100.

View graph

Brocard's conjecture for the indices 1≤n<1001 \le n < 1001≤n<100 (finite verification)

Brocard's conjecture for the indices $1 \le n < 100$ (finite verification)