At Axiom Math, we are building AxiomProver as a serious tool for mathematical research: a system that can take natural-language mathematical statements, and prove it in Lean, meaning the output is 100% verified. In our latest paper, we study a question attached to one of the most mysterious sequences in number theory: when can a value of Ramanujan’s tau function itself be prime? The answer, assuming the abc Conjecture, is that prime values do occur, but they are extraordinarily sparse.
This is a quintessential Ramanujan story because it gathers almost everything that makes his mathematics so magnetic. There is the human story: the self-taught genius from South India, the famous 1913 letter to G. H. Hardy, the Cambridge collaboration, election to the Royal Society, and a life cut short at just 32. There is the mathematics: partitions, q-series, formulas for $\pi$, mock theta functions, and the arithmetic of modular forms. And there is the afterlife of his ideas: Deligne, modular forms, Galois representations, and the long road to Fermat’s Last Theorem.
Our paper focuses on one specific thread in that tapestry. Ramanujan’s tau function produces integers $\tau(n)$ from the Fourier expansion of the discriminant modular form. Those integers behave with uncanny structure. They satisfy multiplicative laws, deep congruences, and subtle growth estimates. Do they ever vanish? That is Lehmer’s famous conjecture, and nobody knows the answer. Can they themselves be prime? That is the question here.
Ramanujan’s long shadow
Ramanujan taught himself from the mathematics he could get his hands on, filled notebooks with startling identities, and then sent Hardy a letter so audacious that Hardy later said the formulas had to be true because nobody could have invented them without being a genius. Hardy brought him to Cambridge, and one of the most remarkable collaborations in the history of mathematics followed. Ramanujan was elected a Fellow of the Royal Society in 1918. He died in 1920 at the age of 32.
Even that short summary understates the scale of the legend. Ramanujan’s work on partitions changed additive number theory. His formulas for $\pi$ still astonish. His mock theta functions were so far ahead of their time that mathematics spent decades catching up. His life later inspired Robert Kanigel’s biography "The Man Who Knew Infinity" and the film adaptation starring Dev Patel and Jeremy Irons. But for this paper, the star is a different Ramanujan creation: $\tau$.
One function, many worlds
Among Ramanujan’s discoveries is the modular form
\[\Delta(z)=q\prod_{n\ge 1}(1-q^n)^{24}=\sum_{n\ge 1}\tau(n)q^n\]
where $q:=e^{2\pi i z}.$ The integers $\tau(1)=1,\ \tau(2)=-24,\ldots$ are the values of Ramanujan’s tau function. A modular form is, very roughly, an analytic function with an extraordinary amount of symmetry, and $\Delta$ is the most famous cusp form of weight 12 on $SL_2(\mathbb{Z})$. That innocent-looking power series hides a remarkable fact: the coefficients $\tau(n)$ behave as if each prime carries its own hidden arithmetic geometry. This is why $\tau$ is not a decorative side character in number theory. It sits very near the center.
One of the earliest clues is Ramanujan’s astonishing congruence modulo 691. If σ₁₁(n) denotes the sum of the 11th powers of the divisors of n, then $\tau(n)\equiv \sigma_{11}(n)\pmod{691}$. For a prime $p$, one gets
\[\tau(p)\equiv 1+p^{11}\pmod{691}.\]
This is a wonderful teaching moment. The right-hand side comes from an Eisenstein series, while the left-hand side comes from the cusp form $\Delta$. So two different modular worlds suddenly become indistinguishable modulo 691.
In the 1960s, Fields medalist Jean-Pierre Serre realized that congruences of this kind were not numerology but evidence of a deeper mechanism. In the hands of Serre, Pierre Deligne, and H. P. F. Swinnerton-Dyer, these congruences became part of the birth of the modern theory of Galois representations.
Image credits
Ramanujan also made a far deeper prediction about the size of $\tau(p)$. For every prime p, he conjectured the sharp size bound displayed below. Deligne proved this through his work on the Weil conjectures. That achievement played a major role in the mathematics that earned him his 1978 Fields Medal. So, the tau function already leads straight into Fields Medal mathematics.
\[|\tau(p)|\le 2p^{11/2}\]
But the Ramanujan bound only tells us how large $\tau(p)$ can be. Another storied conjecture, the Sato-Tate conjecture, asks a subtler question: how are the normalized values distributed inside that allowed interval? The idea is to leverage the fact that $2\cos(\theta)$ maps $[0,\pi]$ to $[-2,2]$ as an order reversing bijection, allowing one to study $\tau(p)/p^{11/2} \in [-2, 2].$ Namely, using angles $\theta_p$ in $[0,\pi]$ that are associated with each prime $p$. From this perspective, Sato-Tate predicts that, as $p$ runs over the primes, those angles are equidistributed with density $\frac{2}{\pi}\sin^2\theta\,d\theta$. In plain language, the normalized values tend to cluster more often near the middle of the interval $[-2,2]$ than near the extremes.
Richard Taylor (Stanford) and his collaborators proved the relevant modular-form version of Sato-Tate, a large part of the work for which Taylor later received the 2015 Breakthrough Prize in Mathematics.
.jpg)
Image credits
This is also why the tau function belongs in the long story of Fermat’s Last Theorem. It would be misleading to say that τ itself proves FLT. The truth is subtler and better: the theories sharpened on $\Delta$—modular forms, congruences, Hecke operators, and especially Galois representations—became part of the toolkit that eventually made FLT possible. So the tau function stands surprisingly close to a Fields Medal, the proof of Fermat’s Last Theorem, and a Breakthrough Prize. That is why it is not just historically important. It is structurally central to modern number theory.
The prime mystery
Despite the crucial role this function has played in developing some of the most profound results in modern mathematics, several seemingly simple problems remain unsolved. As mentioned earlier, we have the famous example of Lehmer’s conjecture, which states that $\tau(n)$ never equals zero. Our paper attacks a different mystery in this landscape: how often can $|\tau(n)|$ itself be prime?
There is a concrete example, and it is a beauty. Lehmer found that:
A concrete prime value \[\tau(251^2)=-80561663527802406257321747\] Its absolute value is prime.
Therefore, prime values of $\tau$ do exist. The question is how often.
Recent work of Xiong had already shown that these prime $\tau$-values form a thin set. This paper proves something much stronger, conditionally on the abc Conjecture.
Main theorem Let $S(X)$ be the number of primes $\ell \le X$ for which $|\tau(n)|=\ell$ for some $n$. Assuming the abc Conjecture, we have \[S(X)=O\!\left(X^{13/22}\right).\] Plain English: only a vanishing fraction of primes ever appear as $|\tau(n)|$.
The abc Conjecture is one of the great unproven conjectures in number theory. Very roughly, it says that if $a+b=c$ and the three numbers share no common factor, then c cannot be too large relative to the product of the distinct prime factors of abc. In this paper, abc becomes a tool for controlling integer solutions to equations that arise from $\tau$.
Turning primes into geometry
The proof begins with a structural fact that already feels surprising: $\tau(n)$ is odd if and only if $n$ is an odd square. Furthermore, the remarkable theory of primitive prime divisors of Lucas sequences allows us to upgrade this fact. It turns out that odd prime values of $\tau$ can only come from prime powers with even exponent $2m$.
For higher exponents $m\ge 3$, earlier work of Xiong already gives strong bounds. The delicate cases are the first two layers: $n=p^2$ and $n=p^4$. Here, the Hecke relations turn the primality question into a geometry problem.
If $\tau(p^2)=\pm \ell$ is prime, then the Hecke operator relation $\tau(p^2)=\tau(p)^2-p^{11}$ can be reformulated as an integer point on a curve of the shape
\[y^2=x^{11}\pm \ell\]
If $\tau(p^4)=\pm \ell$ is prime, a slightly more elaborate algebraic manipulation leads to integer points on curves of the shape
\[u^2=5x^{22}\pm 4\ell\]
So a question that looks at first like pure arithmetic—when is $\tau(n)$ prime?—becomes a question about Diophantine equations. Namely, how often integer points can lie on, or very near, families of hyperelliptic curves?
This is the paper’s main engine. Under the abc Conjecture, we prove that there are not many such near-misses. That estimate handles the $p^2$ and $p^4$ cases. Combined with Xiong’s bounds for the higher layers, it yields the final theorem. The proof is a lovely example of a modern number-theory habit of mind: translate the original question into a shape where structure becomes countable.
Rare is not the same as never
One of the nicest things about the paper is that it does not overclaim. "Misses almost all primes" does not mean "never prime," and it does not even mean "only finitely many prime values." Density zero is much weaker than finiteness.
In fact, the paper ends with a heuristic suggesting that prime values of $|\tau(n)|$ should still occur infinitely often, but just at a tiny microscopic rate. Guided by Sato-Tate, we predict an order of magnitude
\[S(X)\sim C\,\frac{X^{1/11}}{(\log X)^2}\]
In other words, the paper points toward a mathematically delicious possibility: τ may keep hitting primes forever, but so infrequently that the hits disappear statistically inside the ocean of all primes. The function is not forbidden from landing on primes. It is simply astonishingly reluctant to do so.
What AxiomProver actually did
The AI contribution in this project is precise and concrete. AxiomProver was not asked to rediscover all of Ramanujan’s mathematics, or to prove the abc Conjecture, or to rebuild deep outside theorems from scratch. Instead, it was given a sharply defined formalization task:
Inputs. AxiomProver received natural-language statements of the main theorem and key lemmas, a version lock for Lean 4.26.0, the relevant source files from the literature, and explicit instructions that it could assume the abc Conjecture and the cited result of Xiong when needed.
Formalization. It translated the problem into Lean/Mathlib, turning the mathematical statements into machine-checkable objects.
Outputs. It produced problem.lean, containing the formalized statements, and solution.lean, containing a complete formal proof. The human authors then wrote the paper itself (without AI) for human readers.
That distinction matters. AxiomProver did not merely press a button that says "verified." It took a natural-language research problem, built the formal proof engine in Lean, and supplied a machine-checked argument for the paper’s central theorem under the stated assumptions. For mathematical research, that is already a meaningful step toward AI systems that do real proof work.
Artifacts. Readers who want the artifacts can find them here:
arXiv: https://arxiv.org/abs/2603.29970
GitHub: https://github.com/AxiomMath/ramanujan-tau-misses-primes
Journal: https://www.sciencedirect.com/science/article/abs/pii/S001935772600039X