Wikipedia · research solved · AMS 11
hardknown result, no worker yet
Brocard's Conjecture
Theorem · brocard_conjecture.ferreira_large_n
Ferreira proved that Brocard's conjecture is true for sufficiently large n.
Formal statement · Lean 4.lean
theorem brocard_conjecture.ferreira_large_n : ∀ᶠ n in atTop,
letI prev := n.nth Nat.Prime;
letI next := (n+1).nth Nat.Prime;
4 ≤ ((Ioo (prev^2) (next^2)).filter Nat.Prime).card := by
sorryProof. sorry
Nobody has tried yet.