For odd primes p, we let \(K_p:=\mathbb {Q}(\zeta _p)\) be the pth cyclotomic field and let \(\omega \) denote its Teichmüller character. For \(\alpha >1/2\) , we say that an odd prime p is partially regular if the eigenspaces of the p-Sylow subgroup of \({{\,\textrm{Cl}\,}}(K_p)\) under the Galois action vanish for all characters \(\omega ^{p-2k}\) with 1 \(\begin{aligned} 2\le 2k \le \frac{\sqrt{p}}{(\log p)^{\alpha }}. \end{aligned}\) Equivalently, \(p\not \mid {{\,\textrm{num}\,}}(B_{2k})\) throughout this range. We prove that a density-one subset of primes is partially regular in this sense. By Leopoldt reflection, this yields a partial Vandiver theorem: for a density-one set of primes p, the even eigenspaces \(A_p(\omega ^{2k})\) vanish for all even 2k satisfying (1). This result has consequences for Kubota–Leopoldt p-adic L-functions, congruences between cusp forms and Eisenstein series, and p-torsion in algebraic K-groups. The theorem proving partial regularity for almost all p is fully formalized in Lean/Mathlib and was produced automatically by AxiomProver from a natural-language statement of the conjecture.
