Wikipedia · research solved · AMS 11
hardknown result, no worker yet
Legendre's conjecture
Theorem · bounded_gap_legendre
If there exists a constant c > 0 such that
(n + 1).nth Nat.Prime - n.nth Nat.Prime < (n.nth Nat.Prime) ^ (1 / 2 - c) for all large n,
then Legendre's conjecture is asymptotically true.
Formal proof linked here provided by AlphaProof.
Formal statement · Lean 4.lean
theorem bounded_gap_legendre
(H : ∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime <
(n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c)) :
∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p := by
sorryProof. sorry
Nobody has tried yet.