Brocard's conjecture for all indices $n \ge 100$

Open

Brocard.brocard_conjecture_of_ge_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$ , …, $p_{100} = 547$ ). For every index $n \ge 100$ there are at least four primes $q$ with

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

This is Brocard's conjecture restricted to consecutive prime pairs starting from $(p_{100}, p_{101}) = (547, 557)$ ; it is an explicit-threshold strengthening of the asymptotic statement ("for all sufficiently large $n$ ") and remains open.

Preamble

import Mathlib
open Finset Filter

Formal statement

namespace Brocard

theorem brocard_conjecture_of_ge_100 (n : ℕ) (hn : 100 ≤ 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 ; tail (indices ≥ 100) of the statement `brocard_conjecture` (Formal Conjectures, BrocardConjecture.lean).

View graph

Brocard's conjecture for all indices n≥100n \ge 100n≥100

Brocard's conjecture for all indices $n \ge 100$