First coefficients of $\Delta$ : $q-24q^2+252q^3-1472q^4+4830q^5-\cdots$

Proved

RamanujanPetersson.tau_q_expansion

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-formsnumber-theory

Let $\tau(n)$ be Ramanujan's tau function, the coefficients of $\Delta(z)=\sum_n\tau(n)q^n$ . Then the expansion has no constant term and begins

\Delta(z)=q-24q^2+252q^3-1472q^4+4830q^5-\cdots,

that is,

$\tau(0)=0$ , $\tau(1)=1$ ;
$\tau(2)=-24$ , $\tau(3)=252$ ;
$\tau(4)=-1472$ , $\tau(5)=4830$ .

These values pin down the normalisation of $\tau$ and serve as a sanity check of the definition.

Formalization Note $\tau$ is RamanujanPetersson.tau, the $n$ -th coefficient of Mathlib's $q$ -expansion (period $1$ ) of ModularForm.discriminant, valued in $\mathbb C$ .

Preamble

import Mathlib
import Definitions.Def_RamanujanPetersson_tau

open UpperHalfPlane Filter Asymptotics MatrixGroups
open scoped Real

Formal statement

namespace RamanujanPetersson

theorem tau_q_expansion :
    tau 0 = 0 ∧ tau 1 = 1 ∧ tau 2 = -24 ∧ tau 3 = 252 ∧ tau 4 = -1472 ∧ tau 5 = 4830 := by sorry

end RamanujanPetersson

Source

Wikipedia, "Ramanujan–Petersson conjecture", https://en.wikipedia.org/w/index.php?title=Ramanujan%E2%80%93Petersson_conjecture&oldid=1369029052 (PDF snapshot supplied by the proposer, 9 pp.), section "Ramanujan conjecture", displayed expansion

\Delta(z)=\sum_{n=1}^\infty\tau(n)q^n=q-24q^2+252q^3-1472q^4+4830q^5-\cdots

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

First coefficients of Δ\DeltaΔ: q−24q2+252q3−1472q4+4830q5−⋯q-24q^2+252q^3-1472q^4+4830q^5-\cdotsq−24q2+252q3−1472q4+4830q5−⋯

First coefficients of $\Delta$ : $q-24q^2+252q^3-1472q^4+4830q^5-\cdots$