This is the story of formalizing one identity about tenth-order mock theta functions — three days, two essentially different proof strategies, three machine-verified counterexamples to our own intermediate claims, one build server that died at the worst possible moment, and an AI agent whose final 353 lines of uncommitted code, written minutes before it was killed by a session limit, turned out to close the hardest remaining lemma. It is also a story about a piece of advice that sounds too obvious to matter: when you are stuck, reread the original paper.

1. The identity

In Hei-Chi Chan’s An Invitation to q-Series, the chapter on tenth-order mock theta functions culminates in an identity which, stripped to its formal-power-series statement, reads

where $\rho_{r,s}$ is $+1$ on the first quadrant, $-1$ on the third, $0$ elsewhere, and $\delta_3(k)=1$ iff $3\mid k$. The left side is a genuinely mock object — a Hecke-type double sum attached to the indefinite quadratic form $r^2+3rs+s^2$ of discriminant $5$. In an earlier post I described why definite forms (like $c^2+d^2$ in Dobbie’s identity) admit elementary shell-by-shell proofs while indefinite ones resist them. This identity was the test of that resistance.

2. The first road: reduce, reduce, reduce

Our first strategy followed Hickerson and Mortenson: write everything in terms of Appell–Lerch sums $m(x,q,z)$, apply their change-of-z theorem, and reduce the identity to finitely many classical theta facts. This went remarkably far. Along the way we proved, machine-checked and axiom-clean, a small library of genuinely useful theorems:

the formal Jacobi triple product as an infinite arithmetic-progression product,

the Riemann theta relation (Hickerson–Mortenson’s Proposition 1.1) as a finite formal identity, cross-modulus “bridge” identities expressing thetas of modulus $9$, $15$, $18$ in terms of a common level $90$, and a fully formal partial-fraction expansion $\Theta(u)\cdot PF(u) = (q;q)_\infty^3$.

But the final assembly kept receding. Every time an agent reported “one lemma left,” the lemma split. And three times, the discipline of numerically testing every claim before proving it caught us asserting something false:

1. A statement bug. Our cleared form of the change-of-z theorem was stated for all integer parameters. A machine-verified counterexample at $(a,z_0,z_1)=(0,0,1)$ — where a theta factor vanishes — showed the unrestricted statement is simply false. The correct theorem needs a nonsingularity hypothesis, which the book had been carrying implicitly all along.

2. A grading mirage. A large linear-algebra search (Macaulay systems of rank $\sim 10^5$) “proved” our residual identity was outside the span of all Riemann relations. The obstruction was an artifact: we had been treating $K=(Q^{90};Q^{90})_\infty$ as an independent symbol, when in fact every level-90 theta contains one copy of $K$. Counting total $K$-degree correctly ($67 = 67$), the obstruction evaporated — but the identity still wasn’t a Riemann consequence.

3. A window too small. The planned meeting point between the two halves of the proof used coefficient windows that scale only with some of the parameters. A counterexample at $a=186079$ — found numerically, then confirmed when nlinarith refused to prove the needed bound — showed the windows drop nonzero terms for large $|a|$. The false intermediate lemma was deleted, not patched.

Each catch made the formalization more trustworthy. But by the third one it was clear we were tunneling through a mountain sideways.

3. Rereading the book

At that point we did what the remediation checklist says to do first and what everyone actually does last: we went back to the source. Chan’s own proof of the identity occupies three short steps, and its final step is — astonishingly, after our weeks-equivalent of theta algebra — an elementary diagonal extraction. His route:

Step 1 (decoupling). The quadruple sum is the $[x^0y^0]$ constant term of a product of three independent two-variable series:

Step 2 (two lemmas). A lemma of Zwegers evaluates the one-variable factors as theta products; a lemma of Hickerson evaluates the $\rho$-sum as $(q;q)_\infty^3\,\Theta(xy;q)/(\Theta(x;q)\Theta(y;q))$. Chan notes that Hickerson’s lemma can be proved by Dobbie’s method — the same elementary telescoping that closed our definite-form identity weeks earlier.

Step 3 (collapse). Substitute, apply $\Theta(w;q)=-w\,\Theta(wq;q)$ once, and extract the constant term: the three theta sums force the diagonal $k=l=m$, and the surviving single sum is exactly the pentagonal-type series on the right.

The mock-modular depth never went away — it lives inside Zwegers’ lemma. But the architecture of the book’s proof confines all the depth to two self-contained lemmas with elementary proofs, while our first road had smeared the depth across a thirty-one-term cross-modulus residual.

4. The right type for two variables

Formalizing Chan’s route needed something Mathlib does not hand you: bilateral series in two extra variables $x,y$ over $\mathbb Q((Q))$, where $\Theta(x;q)$ has support on all integer powers of $x$. A Hahn series in $x$ won’t do — $\mathbb Z$ with full support is not well-ordered. The resolution is to order exponents $(A,B,C)\mapsto Q^Ax^By^C$ q-adically first:

abbrev ExpQXY := Lex (ℤ × Lex (ℤ × ℤ))   -- (Q-degree, x-degree, y-degree)
abbrev S := HahnSeries ExpQXY ℚ

Because every series in sight has $Q$-degree growing quadratically in its indices, supports are well-ordered in this order even though they are wild in $x$ and $y$ alone. Products are ordinary Hahn multiplication; the constant-term extractor $[x^0y^0]$ is a slice whose well-ordering is inherited through an order embedding. On this foundation the whole proof became:

• Zwegers’ lemma by the functional equation $f(x) = -x^3q^3f(xq^2)$: both sides satisfy the same three-step recurrence in the $x$-degree, so it suffices to match three initial slices — which reduce, via explicit bijections like $\mathbb Z\sqcup\mathbb Z\simeq\{k: 3\nmid k\}$, to two classical product identities, and ultimately to a negative-argument Jacobi triple product $\sum_r z^rq^{T(r)}$ with all-plus signs.
• Hickerson’s lemma by $\rho$-line strings: the coefficient of $x^ay^b$ telescopes along the lines $r+s=\text{const}$; off the diagonal everything cancels against $\Theta(1;q)=0$, and on the diagonal Jacobi’s derivative identity $-\sum_t(-1)^t\,t\,q^{T(t)}=(q;q)_\infty^3$ — already in our library from the Dobbie campaign — produces the cube.
• The collapse and extraction exactly as in the book, plus a transport theorem carrying the result from Hahn series back to the chapter’s stated PowerSeries form.

5. Infrastructure is part of mathematics now

Midway through the final assembly, the build server dropped off the network — for two days. The response turned out to be a good experiment in how much of formalization is actually thinking versus compiling: the agents kept writing Lean offline, validating every step with exact numerics in Python (coefficient tables to $Q^{400}$, three hundred thousand random instances of the index bijections), and queuing the files. When we migrated to a second server — after some disk archaeology to free sixteen gigabytes of old build caches — the six-thousand-line file compiled with thirty-seven errors, every one of them a tactic-strength or name-drift issue, zero of them mathematical. A few hours of fixes later: zero errors, zero sorries.

And one more piece of luck that wasn’t luck: an agent killed mid-flight by a session limit had already written, in its last minutes, the 353 lines that completed the negative-argument triple product. The lines sat uncommitted in a working tree. We tested them — they built cleanly — and committed them as found. Verification doesn’t care who wrote the proof or when.

6. The ledger

The final audit, machine-checked from rebuilt binaries:

— the chapter’s stated target, proved unconditionally; likewise Zwegers’ lemma, Hickerson’s lemma, the decoupling, and the collapse. No sorry, no custom axioms, no native_decide. The full development is now public at github.com/xiangyazi24/invitation-to-qseries-lean.

The first road was not wasted. Its library — the formal triple product, the Riemann relation, the cross-modulus bridges, the partial-fraction machinery — is permanent infrastructure, and its nearly-complete reduction of the change-of-z theorem remains a second, independent route we intend to finish. Two proofs of one identity is not redundancy; for a formal library it is how you sleep at night.

But the lesson of the week is older than Lean: the author of the book already knew the best proof. We spent our cleverness learning to recognize it.

朱熹《观书有感》：

问渠那得清如许？为有源头活水来。

卡了三天的恒等式，答案在书里等了十五年。源头活水，从来不在下游。