At Axiom Math, we are building a tool for the future of mathematical research: an AI that serves as a true thought partner, capable of navigating the rigorous demands of formal proof. As a test case, we asked AxiomProver, the system we are developing, an open problem rooted in the deepest soil of number theory.
In our latest paper, ”Almost All Primes are Partially Regular” (arXiv: https://arxiv.org/abs/2602.05090) we prove a theorem inspired by a question that traces its lineage back to the dawn of algebraic number theory. The "main engine" of this paper was not only checked by a computer; it was also autonomously proved and formalized in Lean by AxiomProver, starting from a natural-language statement.
The Romance of Fermat: A 350-Year Odyssey
To truly appreciate this result, let’s take a step back and look at the most famous marginal note in history. When Pierre de Fermat noted in 1637 that the equation
\[x^n + y^n = z^n\]
has no non-zero integer solutions for $n > 2$, he sparked a quest that would last for centuries and transform the world of mathematics.
The resolution of Fermat’s Last Theorem (FLT) in the 1990s stands as one of the crowning achievements of the 20th century. It required a breathtaking synthesis of ideas: the modularity of elliptic curves, Ken Ribet’s insight (building on Serre’s conjectures) linking Fermat’s equation to modular forms, and the Herculean tour de force by Andrew Wiles and Richard Taylor to prove the semistable Taniyama-Shimura Conjecture.
Image credits
But while Taylor and Wiles wrote the final chapter using the machinery of elliptic curves, Galois representations, and modular forms, the early chapters of this saga forged the very tools we use today to understand the properties of numbers.
The Birth of Algebraic Number Theory
Algebraic number theory and class field theory were largely developed in the attempt to answer Fermat. In the 19th century, mathematicians realized that the "obvious" laws of arithmetic do not hold everywhere. While elementary school students learn that integers factor uniquely into prime numbers (up to order), this fundamental truth can break down in the larger number systems required to study Fermat’s equation, known as rings of algebraic integers. For an odd prime $p$, we care about the Fermat factorization
\[x^p + y^p = \prod_{a=0}^{p-1}\left(x + \zeta_p^{a}y\right)\]
where $\zeta_p := e^{\frac{2\pi i}{p}}$ is a $p$th root of unity. The potential breakdown of unique factorization was the primary obstacle to using this equation to solve FLT for exponent $p$.
Ernst Kummer approached this with a revolutionary idea. He studied the cyclotomic fields generated by $p$-th roots of unity, and he studied their factorization properties. Kummer recognized that if one could measure how badly unique factorization failed, one might still have something to say about FLT.
In modern terminology, he utilized the ideal class group $A_p$, a finite group that quantifies the failure of unique factorization. Kummer’s work gives a clean criterion. If a prime $p$ does not divide the size of this group $A_p$ (a property called $p$-regularity), then Fermat’s Last Theorem is true for that prime exponent $p$.
The Historical Challenge.
This brings us to our work that is based on a refinement of Kummer’s work. The class group is not a monolithic object. Under the action of the Galois group, it decomposes into eigenspaces.
\[A_p \cong \bigoplus_{i=0}^{p-2} A_p\!\left(\omega^i\right)\]
Where Kummer saw a single block, this decomposition reveals a mosaic. It splits the class group into independent pieces, allowing us to prove that specific parts vanish even if the whole remains unknown. Crucially, this decomposition splits into two distinct halves. The odd part which is now understood by the work of Jacques Herbrand and Ken Ribet. But the even part remains a complete mystery.
Vandiver’s Conjecture. For every odd prime $p$, the even part is trivial.
The conjecture can be refined using eigenspaces in the following form.
Conjecture (Kummer-Vandiver $[7, 19]$). If $p$ is an odd prime then we have \[A_p\!\left(\omega^{2k}\right)=0 \quad \text{for all even } 2k\in\{2,4,\ldots,p-3\}\]
A Partial Vandiver Result for Almost All Primes
We establish a "Partial Vandiver Conjecture" for a density 1 subset of primes. Specifically, we prove the vanishing, for almost all primes, that the even eigenspaces in the range
\[A_p(\omega^2)=A_p(\omega^4)=\cdots=A_p\!\left(\omega^{2M_\alpha(p)}\right)=0\]
where
\[M_\alpha(p):=\left\lfloor\frac{\sqrt{p}}{(\log p)^\alpha}\right\rfloor\]
This result is not an isolated fact, and its proof is far from a one-liner. It is the consequence of a beautiful mathematical synthesis that combines:
Herbrand-Ribet Theorem: Linking the odd eigenspaces to Bernoulli numbers.
Euler’s Formula: Connecting Bernoulli numbers to the Riemann zeta function.
Leopoldt’s Reflection Principle: A "mirror" theorem that reflects information from the well-understood odd part back into the mysterious even part.
Image credits
The logic proceeds as follows: We analyze the "partial regularity" of Bernoulli numbers. If a prime is regular in a specific range, Herbrand-Ribet implies the odd eigenspaces vanish. Leopoldt’s reflection principle then forces the corresponding even eigenspaces to vanish as well.
The AI Experiment: AxiomProver’s Role
This brings us to the core of our case study. The mathematical heart of this argument, the "engine" that establishes the density of these primes is Theorem 1.3 on arXiv: https://arxiv.org/abs/2602.05090. A prime $p$ is $M$-regular if $p$ does not divide the numerator of the Bernoulli numbers for all even indices in the range $B_2, B_4, \ldots, B_{2M}$.
Theorem 1.3. If $\alpha > \frac{1}{2}$, then there exists a constant $C_\alpha > 0$ such that as $X \to +\infty$ we have \[\#\{\,p \le X \text{ prime} : p \text{ is not } M_\alpha(p)\text{-regular}\,\}\le C_\alpha \frac{X}{(\log X)^{2\alpha}}\]
We presented AxiomProver with the natural-language statement of this density theorem. We did not ask it to re-prove the deep external theorems of Ribet or Leopoldt. Rather, we asked it to construct the analytic proof that links these concepts to the distribution of primes.
The result? AxiomProver autonomously generated a correct, fully verified proof in Lean/Mathlib from the natural-language statement of Theorem 1.3.
How AxiomProver produced the proof
We describe the workflow, with links for those who want to dive into the details.
1. The Inputs (Natural-language statement)
We provided AxiomProver with a natural-language formulation of Theorem 1.3 together with a self-contained list of definitions.
2. Formalization in Lean
AxiomProver translated the statement into Lean, reusing Mathlib’s infrastructure for Bernoulli numbers and the Prime Number Theorem
3. Automated lemma proving and bookkeeping
AxiomProver generated the complete argument, with Lean checking the proof in its entirety.
4. Artifacts
The outputs are:
the human-readable paper on arXiv: https://arxiv.org/abs/2602.05090,
GitHub for the machine-checked Lean proof: https://github.com/AxiomMath/partial-regularity
What Did We Learn?
This experiment taught us something vital about the current capabilities of our AxiomProver. To prove this theorem, our system had to expertly wield the standard tools of a domain expert in analytic number theory:
Facts about Bernoulli numbers
Euler’s formulas for Riemann’s zeta at negative odd integers,
The Prime Number Theorem.
The AI didn’t just stumble upon a solution; it assembled a proof. It demonstrated that it can "think" like an analytic number theorist, bridging the gap between high-level conjectures and the nuts-and-bolts of rigorous verification. As we continue to develop AxiomProver, this case study stands as evidence that AI can be more than a calculator, it can make contributions to number theory.