In 1920, Ramanujan wrote his last letter to Hardy, describing a new class of functions he called “mock theta functions.” Among the most mysterious are the tenth-order mock theta functions, whose identities resisted proof for decades until Choi (1999), Zwegers (2002), and Hickerson–Mortenson (2010) developed the necessary machinery. This post describes the formal verification — in Lean 4 — of one such identity, and the unexpected new proof method that emerged from the formalization effort.

The identity

The theorem, following Chapter 10 of H.-C. Chen’s An Invitation to q-Series, states that the Hecke-type double sum $f\_{2,3,2}$ equals the Appell–Lerch sum $\hat{G}$ as two-variable formal Hahn series:

where $F\_{\mathrm{hm}}$ is a signed sum over a cone in $\mathbb{Z}^2$ (the “Hecke double sum”) and $\hat{G}(1)$ is constructed from Appell–Lerch quotients $M(a,z) = N(a,z)/j(z;q)$ via localized inverses in the Hahn series ring.

The Hecke side has coefficients supported on the “same-sign cone” $\\{(r,s) : r \geq 0,\, s \geq 0\\} \cup \\{(r,s) : r < 0,\, s < 0\\}$. The Appell–Lerch side has support everywhere. The identity says these two very different objects are equal as elements of $S = \mathrm{HahnSeries}\;\mathrm{Exp}\_{QXY}\;\mathbb{Q}$.

The formalization framework

The proof lives entirely in the Hahn series ring $S$ — a commutative ring of formal series indexed by a partially well-ordered monoid, with coefficients in $\mathbb{Q}$. No analytic convergence, no complex variables, no modular forms. The key algebraic facts:

• $S$ has no zero divisors (a Mathlib instance: NoZeroDivisors S).
• Localized inverses $\mathrm{locInv}(B)$ satisfy $\mathrm{locInv}(B) \cdot B = 1$ for nonzero $B$.
• The Appell–Lerch numerator satisfies a two-variable functional equation (the “Appell FE”) proved at the series level.

The existing infrastructure included a proved Hecke-side coefficient normal form:

where $\Omega$ is an explicit formula involving the same-sign indicator $\mathrm{sg}(x-2v, y+2v)$ and a quadratic $q$-degree polynomial $\Phi(x,y,u,v)$.

The multi-day struggle

The goal was to prove the matching identity for the Appell side:

where $\mathrm{Mhat} = P\_Y \cdot B\_X + P\_X \cdot B\_Y$ is the boundary-cleared Appell numerator sum.

Six approaches were tried and eliminated:

1. Per-side $q$-periodicity. Each side individually is not $q$-periodic — only their difference is (because it is zero). This killed the “off-diagonal telescope” strategy.

2. Pointwise $(r,l) \to (u,v)$ bijection. The $q$-degree maps match (proved by ring), but the signs do not match pointwise. The identity holds only at the summed level.

3. $J\_1^3$ diagonal collapse. The full diagonal slice $\mathrm{coeff}\_{XY}(F\_{\mathrm{hm}} \cdot B\_Y \cdot B\_X)(t,t)$ is not a $J\_1^3$ series — it has a more complex multi-index structure.

4. $S$-level decomposition. Writing $\mathrm{clearedD} = B\_Y B\_X(F\_{\mathrm{hm}} - I\_Y - I\_X) + x\_Y B\_X + x\_X B\_Y$ is algebraically correct but the remaining identity is equivalent to $\mathrm{clearedD} = 0$ — circular.

5. Individual pair bridges. The Y-pair bridge depended on a sorry stub that was false (the sheared-tail lemma). The X-pair bridge was circular.

6. FE + uniqueness (the textbook approach). This requires Ghat’s functional equation, which requires the pair FEs, which require the bridges — circular.

And the longest-lasting obstacle: a Python verification script with a bug. It missed contributions from one of the four Appell rows (R3, at non-lex-positive denominators), producing four “counterexamples” that appeared to prove the two-variable identity was false. This blocked progress for multiple sessions until independent exact-integer verification showed all four counterexamples were wrong.

The breakthrough: wall coordinates and a parity miracle

The proof that finally worked proceeds in four stages.

Stage 1: Parity split. The four-row Appell sum splits by the parity of $(x, y)$: even $x$ activates rows R0/R2, even $y$ activates R1/R3. At each $(x,y)$, exactly two rows contribute. This is proved by showing wrong-parity rows have zero coefficients (the $x$-component of the raw exponent is always even for R0 and always odd for R2, etc.).

Stage 2: Finsum reindex. For each contributing row, the four-index finsum over $(k, r, t, m)$ collapses to a two-index finsum over $(r, l)$ at “on-shell” coordinates. The collapse uses an explicit coordinate equivalence (R0CoordEquiv, etc.) and the fact that off-shell terms have zero coefficients (by the $x/y$ constraint). This is the step that required the most Lean engineering — finsum_comp_equiv for the reindex, finsum_coord_drop_error for the off-shell vanishing.

Stage 3: The involution defect. After reindexing, the two-row coefficient at $(U,V)$ is:

while the Hecke $\Omega$-coefficient is $(-1)^V \cdot \mathrm{sg}(a-V,\, b+V)$. These are not pointwise equal. Their difference — the “cross-$V$ defect” — decomposes as two finite wall functions:

Stage 4: The root-pair involution. Change coordinates to $p = U+V-a-1$, $q = -U-a$. Then $\Phi$ becomes a symmetric quadratic in $(p,q)$:

with $L = 2a + 4b + 5$. The key observation: $L$ is always odd. This means the root-pair involution

has no integer fixed point (since $2q = 8p + L$ has no integer solution when $L$ is odd), preserves $\Psi$, and flips $(-1)^{p+q}$. Therefore the defect sum over each $\Psi$-fiber cancels pairwise, giving zero.

The five core lemmas — qInvL_invol, qInvL_preserves_Psi, qInvL_no_fix, qInvL_flips_parity, and Psi_swap — are each one-liners proved by ring or omega.

How this differs from the textbook proof

Chen’s proof (following Zwegers 2010) uses an entirely different method:

1. Rewrite the identity using Zwegers’ Theorem 10.1 (mod-3 functions).
2. Apply Hickerson’s Lemma 10.2, which connects the Hecke cone to a theta quotient via Ramanujan’s ${}\_1\psi\_1$ summation.
3. Factor and extract the $[x^0 y^0]$ coefficient.

This is an analytic/one-variable approach that specializes the two-variable identity to one variable before proving it. Our proof works directly in the two-variable Hahn series ring, never specializes, and replaces the ${}\_1\psi\_1$ machinery with the finite algebraic cancellation described above. The root-pair involution with the parity constraint $L \equiv 1 \pmod{2}$ does not appear in any of the existing proofs (Hickerson 1988, Choi 1999, Zwegers 2010, Hickerson–Mortenson 2010).

Scale

The total output: 30 commits, approximately 3000 lines of new Lean 4 code, with zero sorry and clean #print axioms (only propext, Classical.choice, Quot.sound).

What’s next

The proved identity $F\_{\mathrm{hm}} = \hat{G}(1)$ is the core of Chapter 10 in Chen’s book. Downstream, it feeds into the kernel statements (theta correction identities) that connect to the classical mock theta conjectures. Those remain as open sorry stubs — the next campaign.

Whether the root-pair involution proof constitutes a genuinely new proof of the Hickerson–Mortenson identity, or merely a new formalization route for a known result, is a question for the experts. The algebraic mechanism — symmetric quadratic with odd linear parameter forcing fixed-point-free involution — may have applications to other Hecke-type identities where the ${}\_1\psi\_1$ approach is available but difficult to formalize.

「看似寻常最奇崛，成如容易却艰辛。」—— 王安石《题张司业诗》

“What looks ordinary is in truth most remarkable; what seems easy was in fact most arduous.” — Wang Anshi, “On the Poetry of Zhang Sigong”