Almost all primes are partially regular
Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta, Ishan Sinha, Jimmy Xin, Jujian Zhang
TL;DR
The paper proves that almost all odd primes are partially regular: for any fixed \alpha>\tfrac12$ and $M_{\alpha}(p)=\left\lfloor\frac{\sqrt{p}}{(\log p)^{\alpha}}\right\rfloor$, a density-one set of primes $p$ satisfy that $p\nmid \text{num}(B_{2k})$ for all even $2\le 2k\le M_{\alpha}(p)$. The argument centers on Bernoulli-number divisibility, via the quantities $P_m=\prod_{k=1}^m|\text{num}(B_{2k})|$ and the primorial bound $\omega_{pf}(n) \le C\log n/\log\log n$, together with a reduction from the variable range $M_{\alpha}(p)$ to a fixed $m_X$, yielding the bound $\#\{p\le X:\ p\text{ not }M_{\alpha}(p)\text{-regular}\} \le C_α X/(\log X)^{2\alpha}$. Through Leopoldt reflection this implies a partial Vandiver result for a density-one subset of primes, and it has further implications for Kubota-Leopoldt $p$-adic $L$-functions, modular form congruences, and higher $K$-theory. The work is additionally presented as a fully formalized Lean/Mathlib proof generated by the AI tool AxiomProver, illustrating a novel AI-assisted approach to mathematical verification, with detailed protocol and case-study analysis.
Abstract
For odd primes $p$, we let $K_p:=\mathbb{Q}(ζ_p)$ be the $p$th cyclotomic field and let $ω$ denote its Teichmuller character. For $α>1/2$, we say that an odd prime $p$ is partially regular if the eigenspaces of the $p$-Sylow subgroup of $\operatorname{Cl}(K_p)$ under the Galois action vanish for all characters $ω^{p-2k}$ with \[ 2\le 2k \le \frac{\sqrt{p}}{(\log p)^α}. \] Equivalently, $p\nmid \operatorname{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(ω^{2k})$ vanish for all even $2k$ satisfying the inequality above. 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.