ABC implies that Ramanujan's tau function misses almost all primes
David Kurniadi Angdinata, Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Simon Mahns, Aram H. Markosyan, Rithikesh Muddana, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta, Ishan Sinha, Jimmy Xin, Jujian Zhang
math.NT
Mar 31, 2026 · v1
TL;DR
The main engine was formalized automatically in Lean/Mathlib by AxiomProver from a natural-language statement.
Abstract
Lehmer conjectured that Ramanujan's tau-function never vanishes. In a related direction, a folklore conjecture asserts that infinitely many primes arise as absolute values of Ramanujan's tau-function. Recently, Xiong showed that these prime values form a subset of the primes with density at most $2/11$. Assuming the $abc$ Conjecture, we prove the stronger upper bound \[ S(X):=\#\{\ell\le X:\ \ell\ \text{prime and } |τ(n)|=\ell \text{ for some } n\ge 1\} = O(X^{13/22}), \] which implies that Ramanujan's tau-function misses a density 1 subset of the primes. We give a heuristic suggesting that $S(X)$ should nevertheless be infinite, with predicted order of magnitude \[ S(X)\asymp \frac{C X^{\frac{1}{11}}}{(\log X)^2}. \] The main engine in this note was formalized and produced automatically in Lean/Mathlib by AxiomProver from a natural-language statement of the problem.
Problem
A folklore conjecture asserts that infinitely many primes arise as absolute values of Ramanujan's tau-function. Xiong recently showed these prime values form a subset of the primes with density at most 2/11, but tighter bounds conditional on standard conjectures were not known.
Approach
Assuming the abc Conjecture, the authors translate solutions to tau(p^{2k}) = +/- l into integral points on a hyperelliptic curve, then count these points using bounds from the abc conjecture. The main engine of the proof was formalized and produced automatically in Lean/Mathlib by AxiomProver from a natural-language statement of the problem.
Results
Assuming abc, the authors prove S(X) := #{l <= X : l prime and |tau(n)| = l for some n} = O(X^{13/22}), implying that Ramanujan's tau-function misses a density-1 subset of the primes. They also provide a heuristic suggesting S(X) should be infinite with predicted order X^{1/11}/(log X)^2.
