Wikipedia · research open · AMS 11
unsolvedsorry — nobody on it
Brocard's Conjecture
Conjecture · brocard_conjecture
**Brocard's Conjecture**
For every n ≥ 2, between the squares of the n-th and (n+1)-th primes,
there are at least four prime numbers.
Formal statement · Lean 4.lean
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
sorryProof. sorry
Nobody has tried yet.