ABC implies that Ramanujan's tau function misses almost all primes

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 } |\tau(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.