Brocard's Conjecture

Reference: Wikipedia

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.