cohen_lenstra_heuristics
Disprovedalgebraalgebraic-geometrymillennium-prize
Cohen–Lenstra heuristics (1984): The distribution of p-parts of class groups of imaginary quadratic fields follows a specific probability distribution related to random abelian p-groups. Numerical evidence is strong; rigorous proof is open. Connected to BSD conjecture and random matrix theory.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem cohen_lenstra_heuristics :
∀ (p : ℕ) (hp : Nat.Prime p) (eps : ℝ) (_ : 0 < eps),
∃ (C rho : ℝ), 0 < rho ∧ rho < 1 ∧
(∀ (N : ℕ) (_ : 1 ≤ N),
|({D : Fin N | ∃ r : ℕ, 1 ≤ r ∧ p ^ r ∣ N}.ncard : ℝ) / N - rho| ≤
C * (N : ℝ) ^ (-1/2 + eps)) := by
sorrySource