Motivation

For $n \ge 1$ let $p_n$ denote the $n$-th prime. Brocard's conjecture, named after Henri Brocard, asserts that for every $n \ge 2$ there are at least four primes strictly between $p_n^2$ and $p_{n+1}^2$ (Wikipedia). It belongs to the family of "primes between consecutive squares" problems together with Legendre's conjecture, and it is a concrete, elementary-looking question about short-interval prime distribution that remains open.

Timeline

• Early 20th century — Brocard states the conjecture.
• 2023 — L. A. Ferreira (arXiv:2307.08725) proves that the conjecture holds for all sufficiently large $n$.

Setting

Primes are listed in increasing order. In the Lean development the list is 0-indexed: Nat.nth Nat.Prime k is the $k$-th prime counting from $0$, so nth 0 = 2, nth 1 = 3, nth 2 = 5, and so on. For an index $n$ write $\mathrm{prev} =$ n.nth Nat.Prime and $\mathrm{next} =$ (n+1).nth Nat.Prime, two consecutive primes. The quantity of interest is

$$\#\{\, q \text{ prime} : \mathrm{prev}^2 < q < \mathrm{next}^2 \,\}.$$

Target

Milestone (Ferreira): for all sufficiently large indices $n$,

$$4 \le \#\{\, q \text{ prime} : \mathrm{prev}^2 < q < \mathrm{next}^2 \,\}.$$

Goal (Brocard's conjecture): the same inequality for every 0-indexed $n \ge 1$, i.e. for every pair of consecutive primes starting from $(3,5)$.

Significance

A proof of the goal settles Brocard's conjecture outright. Given Ferreira's asymptotic result, the remaining work splits into making the threshold effective and closing the finite range below it, both of which would be new formal content; the milestone itself (formalizing Ferreira's analytic argument) is a substantial analytic-number-theory formalization project.

Difficulty

Unconditional results on primes in short intervals $[x, x + x^{\theta}]$ only reach exponents $\theta$ well above $1/2$, while the interval $(p_n^2, p_{n+1}^2)$ has length about $2 p_n g_n$ where $g_n = p_{n+1} - p_n$ can be small (e.g. twin primes), i.e. length on the order of the square root of its endpoint. Standard short-interval theorems therefore do not apply uniformly, and Legendre's conjecture — which would only give two primes here — is itself open.

Formalization scope

Everything is stated with Mathlib's Nat.nth Nat.Prime, Finset.Ioo (open interval, endpoints excluded) and Finset.filter Nat.Prime, followed by Finset.card. The hypothesis 1 ≤ n in the goal is the 0-indexed form of the source's "$n \ge 2$"; it is necessary, since for index $0$ (primes $2, 3$) the interval $(4, 9)$ contains only the two primes $5, 7$. The milestone uses Filter.atTop ("for all sufficiently large $n$"), with no explicit threshold. No custom definitions are required.

Selected references

• Brocard's conjecture, Wikipedia. https://en.wikipedia.org/wiki/Brocard%27s_conjecture
• L. A. Ferreira, Real exponential sums over primes and prime gaps, arXiv:2307.08725 (2023). https://arxiv.org/abs/2307.08725
• Statement adapted from the Formal Conjectures project (Apache-2.0), file BrocardConjecture.lean.