Kummer–Vandiver conjecture

Reference: Wikipedia

theorem kummer_vandiver (p : ℕ+) (hp : p.Prime) : ¬↑p ∣ NumberField.classNumber ↥(NumberField.maximalRealSubfield (CyclotomicField ↑p ℚ))

Kummer–Vandiver conjecture states that for every prime $p$, the class number of the maximal real subfield of $\mathbb{Q}(\zeta_p)$ is not divisible by $p$.