Almost all primes are partially regular

Technical Summary: "Almost All Primes Are Partially Regular"

Problem Statement
The paper addresses the distribution of irregularities in the arithmetic of cyclotomic fields. For an odd prime $p$, let $K_p = \mathbb{Q}(\zeta_p)$ be the $p$-th cyclotomic field and $Cl(K_p)$ its ideal class group. A prime $p$ is classically defined as regular if $p$ does not divide the class number $|Cl(K_p)|$, a condition equivalent to $p$ not dividing the numerator of any Bernoulli number $B_{2k}$ for $2 \le 2k \le p-3$. While irregular primes are known to exist (Jensen), their density is conjectured to be approximately $1 - e^{-1/2}$.

The authors investigate a weaker notion termed partial regularity. An odd prime $p$ is defined as $m$-regular if $p \nmid \text{num}(B_{2k})$ for all even integers $2k$ in the range $2 \le 2k \le \min(m, p-3)$. The central question is whether a "density-one" subset of primes satisfies partial regularity for a specific range $M_\alpha(p)$ that grows with $p$, specifically $M_\alpha(p) \approx \sqrt{p}/(\log p)^\alpha$ for $\alpha > 1/2$.

Methodology
The proof of the main theorem relies on analytic number theory techniques involving the growth of Bernoulli number numerators and the distribution of prime divisors. The methodology proceeds as follows:

1. Reduction to a Uniform Range: The authors define a uniform bound $m_X = \lfloor \sqrt{X}/(\log X)^\alpha \rfloor$ for primes $p \le X$. They show that if a prime $p \le X$ fails to be $M_\alpha(p)$-regular, it must also fail to be $m_X$-regular (for sufficiently large $X$).
2. Bounding Irregular Primes: Using Lemma 2.1, the number of primes $p \le X$ that are not $m_X$-regular is bounded by $\omega_{pf}(P_{m_X})$, where $P_{m_X}$ is the product of the numerators of Bernoulli numbers $B_{2k}$ for $1 \le k \le m_X$, and $\omega_{pf}(n)$ denotes the number of distinct prime factors of $n$.
3. Estimating Bernoulli Numerators: The authors derive an upper bound for $\log |P_m|$ using Euler's formula for $\zeta(2k)$ and the von Staudt–Clausen theorem. They establish that $\log P_m \le C_2 m^2 \log m$.
4. Prime Factor Counting: Applying the Prime Number Theorem and properties of the primorial function, they bound $\omega_{pf}(P_{m_X})$ by $C_3 \frac{\log P_{m_X}}{\log \log P_{m_X}}$.
5. Asymptotic Analysis: Combining these estimates, the count of non-regular primes is shown to be bounded by $O\left(\frac{X}{(\log X)^{2\alpha}}\right)$. Since $\alpha > 1/2$, the exponent $2\alpha > 1$, ensuring that the density of non-regular primes tends to zero as $X \to \infty$.

Key Contributions and Results
The paper establishes the following main result:

• Theorem 1.1: For any fixed $\alpha > 1/2$, the set of primes $p$ that are not $M_\alpha(p)$-regular has asymptotic density zero. Specifically, the number of such primes up to $X$ is bounded by $C_\alpha \frac{X}{(\log X)^{2\alpha}}$. The authors note that the constant $C_\alpha$ can be chosen independently of $\alpha$ (specifically $C_\alpha = 10$).

Corollaries and Implications
The paper derives several significant consequences from this partial regularity result:

1. Partial Vandiver Theorem (Corollary 1.4): By combining Theorem 1.1 with the Herbrand–Ribet Theorem (linking odd eigenspaces of the class group to Bernoulli numbers) and Leopoldt's Reflection Principle (linking even and odd eigenspaces), the authors prove that for a density-one set of primes, the even eigenspaces $A_p(\omega^{2k})$ of the $p$-part of the class group vanish for all $2k \le M_\alpha(p)$. This provides a partial verification of the Kummer–Vandiver Conjecture.
2. Non-vanishing of $p$-adic $L$-functions (Corollary 1.5): Via the Iwasawa Main Conjecture (Mazur–Wiles), the vanishing of the algebraic eigenspaces implies that the associated Kubota–Leopoldt $p$-adic $L$-functions $L_p(s, \omega^{2k})$ are units in the Iwasawa algebra $\Lambda = \mathbb{Z}_p[[T]]$. Consequently, for almost all primes, these functions have no zeros in $\mathbb{Z}_p$.
3. Congruences and K-Theory (Corollary 1.7): The result implies that for almost all primes:
   • Specific power sum congruences involving Bernoulli numbers hold modulo $p^2$.
   • There are no congruences between normalized cuspidal Hecke eigenforms of level 1 and weight $2k$ and Eisenstein series modulo $p$ for small weights.
   • The algebraic K-groups $K_{4k-2}(\mathbb{Z})$ have no $p$-torsion for these weights.

Significance and Verification
The paper highlights two primary aspects of its significance:

1. Mathematical Result: It provides a rigorous proof that "almost all" primes satisfy a strong form of partial regularity, extending the understanding of the distribution of irregular primes and offering a partial resolution to the Vandiver Conjecture in a specific range.
2. Formalization and AI: The paper serves as a case study for AxiomProver, an AI tool under development. The authors state that Theorem 1.1 was proven and fully formalized in Lean/Mathlib (version 4.26.0) by AxiomProver starting solely from a natural-language statement of the conjecture, without human assistance in the proof generation. The human authors then reconstructed the narrative exposition based on the formal proof. The code and artifacts are publicly available in the AxiomMath repository.

The authors emphasize that the AI did not reprove deep external theorems (like Herbrand–Ribet or the Main Conjecture) but autonomously derived the specific analytic estimate required for Theorem 1.1, including an independent derivation of a bound related to the von Staudt–Clausen theorem.