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

Source: arxiv:2603.29970 Authors: Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang Status: verified Main declarations: main_theorem, reduction_lemma, abc_bound_E2, abc_bound_E4 Tags: number-theory, modular-forms MSC: 11F30, 11N05

Mathematical overview

Ramanujan's tau function τ : ℤ_{≥1} → ℤ is the sequence of Fourier coefficients of the modular discriminant. It is axiomatised here through a structure RamanujanTau recording five of its standard properties: Hecke multiplicativity, the Hecke recurrence at prime powers, the parity criterion (τ n is odd iff n is an odd perfect square), Deligne's bound |τ p| ≤ 2 p^{11/2}, and the non-unit property τ n ≠ ±1 for n ≥ 2.

Define the counting function S(X) = #{ ℓ ≤ X : ℓ prime, |τ n| = ℓ for some n ≥ 1 }. Assuming the ABC conjecture and (the sharper N^{1/2} form of) Xiong's Proposition 5.4, the main theorem main_theorem shows S(X) = O(X^{13/22}), i.e. the tau function takes prime absolute values at a density-zero set of primes. The argument passes through a reduction lemma (reduction_lemma) bounding S(X) by error terms E₂(X) and E₄(X) counting near-misses of x^{11} by squares and of 5 x^{22} by squares, and ABC-driven bounds on those error terms (abc_bound_E2, abc_bound_E4).

Provenance

Imported from https://github.com/AxiomMath/ramanujan-tau-misses-primes; initial code generated by Axiom Math, accompanying the paper arXiv:2603.29970. Upstream contains no sorrys in the solution file. Ported from Lean v4.26.0 to Lean Pool's v4.30.0-rc2.