Andrica's conjecture

References:

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

theorem Andrica.andrica_conjecture (n : ℕ) : √↑(Nat.nth Nat.Prime (n + 1)) - √↑(Nat.nth Nat.Prime n) < 1

Andrica's conjecture The inequality $\sqrt{p_{n+1}}-\sqrt{p_n} < 1$ holds for all $n$, where $p_n$ is the $n$-th prime number.

theorem Andrica.andrica_conjecture.ferreira_large_n : ∀ᶠ (n : ℕ) in Filter.atTop, √↑(Nat.nth Nat.Prime (n + 1)) - √↑(Nat.nth Nat.Prime n) < 1

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