Andrica's conjecture

Reference: Wikipedia

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 nth prime number.