Legendre's conjecture

References:

• Landau Problems Wikipedia Page
• Legendre Conjecture Wikipedia Page
• Luan Alberto Ferreira, Real exponential sums over primes and prime gaps

theorem LegendreConjecture.legendre_conjecture : sorry ↔ ∀ n ≥ 1, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Prime p

Does there always exist at least one prime between consecutive perfect squares?

theorem LegendreConjecture.legendre_conjecture.ferreira_large_n : ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Prime p

Ferreira proved that the conjecture is true for sufficiently large n.