Brocard's Conjecture

References:

• Wikipedia
• Luan Alberto Ferreira, Real exponential sums over primes and prime gaps

theorem Brocard.brocard_conjecture (n : ℕ) (hn : 1 ≤ n) : 4 ≤ (Finset.filter Nat.Prime (Finset.Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2))).card

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.

theorem Brocard.brocard_conjecture.ferreira_large_n : ∀ᶠ (n : ℕ) in Filter.atTop, 4 ≤ (Finset.filter Nat.Prime (Finset.Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2))).card

Ferreira proved that Brocard's conjecture is true for sufficiently large n.