Brocard's conjecture holds for all sufficiently large n (Ferreira)

Open

Brocard.brocard_conjecture.ferreira_large_n

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

number-theoryprime-gapsprimes

There is an $N$ such that for every $n \ge N$ , writing $p_n$ for the $n$ -th prime (0-indexed: $p_0 = 2$ ), there are at least four primes $q$ with $p_n^2 < q < p_{n+1}^2$ .

Preamble

import Mathlib
open Finset Filter

Formal statement

namespace Brocard

theorem brocard_conjecture.ferreira_large_n : ∀ᶠ n in atTop,
    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

L. A. Ferreira, Real exponential sums over primes and prime gaps, arXiv:2307.08725 (2023); statement as in Formal Conjectures, BrocardConjecture.lean, `brocard_conjecture.ferreira_large_n`

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. There exists a threshold $N$ such that for every natural number $n \ge N$ (this is ∀ᶠ n in Filter.atTop): with $\mathrm{prev} =$ Nat.nth Nat.Prime n and $\mathrm{next} =$ Nat.nth Nat.Prime (n+1) (consecutive primes, 0-based indexing), the number of primes $q$ with $\mathrm{prev}^2 < q < \mathrm{next}^2$ (both inequalities strict) is at least $4$ .

Checks. No explicit value of $N$ is asserted, so this is an ineffective "for all sufficiently large $n$ " statement, matching the reported result of Ferreira (arXiv:2307.08725). It is strictly weaker than the goal Brocard.brocard_conjecture (which asserts the bound for all $n \ge 1$ ) and follows from it; it is not vacuous, since it constrains all but finitely many indices.

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