Brocard's Conjecture

Reference: Wikipedia

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

For every n ≥ 2, between the squares of the n-th and (n+1)-th primes, there are at least four prime numbers.