The Weight Comes Last

Often in mathematics, a problem with a simple, easy-to-describe premise turns into a much deeper problem requiring expertise to even understand the statement. This blog post tells the story of the opposite. Here, a Riemann hypothesis for a certain zeta function turns into the most elementary mathematics of all: looking for carries in grade-school addition.

This blog post will give a quick overview of our recent paper on Thakur's hypotheses. The paper itself is too technical to describe in its entirety, but we'll cover:

1. The definition of the zeta function and the degrees that we're interested in.
2. A walkthrough of the case $d = 1$, using Taylor series and Lucas' theorem as the primary weapons.
3. A description of Thakur's three hypotheses we formally proved.
4. A few brief notes on our formalization process.

The Riemann zeta function $\frac{1}{1^s}+\frac{1}{2^s}+\frac{1}{3^s}+\frac{1}{4^s}+\cdots$ is famous for being the namesake of the Riemann hypothesis, but in mathematics there are actually a lot of other kinds of functions like it. Our recent paper on Thakur's hypotheses is based on a different zeta function called the Carlitz-Goss zeta function, which we'll define now.

In this post, we'll fix a prime $q$, and always work modulo $q$. A monic polynomial $a(t)$ is one whose leading coefficient is $1$ (and whose other coefficients can be any of $0$, $1$, ..., $q-1$). The Carlitz-Goss zeta function $\zeta(k)$ is defined by summing $a^{-k}$ over all such $a(t)$. For example, when $q = 3$, the first several fractions in the sum are

$$\begin{aligned}\zeta(k)&=\frac{1}{1^k}+\frac{1}{t^k}+\frac{1}{(t+1)^k}+\frac{1}{(t+2)^k}\\&\quad+\frac{1}{(t^2)^k}+\frac{1}{(t^2+1)^k}+\frac{1}{(t^2+2)^k}\\&\quad+\frac{1}{(t^2+t)^k}+\frac{1}{(t^2+t+1)^k}+\cdots\end{aligned}$$

(One can also define multi-zeta functions $\zeta(k_1,\ldots,k_r)$ in several variables too, or when $q$ is a prime power instead of just a prime --- but that's beyond the scope of this blog post.)

Like its Riemann counterpart, the Carlitz-Goss zeta function also has a Riemann hypothesis about the zeros of the zeta function, among other results. But this version of the Riemann hypothesis is much easier to prove, and in fact it follows directly from one of the three hypotheses we establish in our paper.

To break down $\zeta(k)$ into more manageable parts, we'll let $S_d (k)$ denote the contribution of just the degree-$d$ polynomials. Continuing the example when $q = 3$, the $d=1$ part is the sum over the three monic linear polynomials:

$$S_1(k)=\frac{1}{t^k}+\frac{1}{(t+1)^k}+\frac{1}{(t+2)^k}.$$

Then, $S_2(k)$ is the sum over nine monic quadratic polynomials:

$$\begin{aligned}S_2(k)&=\frac{1}{(t^2)^k}+\frac{1}{(t^2+1)^k}+\frac{1}{(t^2+2)^k}\\&\quad+\frac{1}{(t^2+t)^k}+\frac{1}{(t^2+t+1)^k}+\frac{1}{(t^2+t+2)^k}\\&\quad+\frac{1}{(t^2+2t)^k}+\frac{1}{(t^2+2t+1)^k}+\frac{1}{(t^2+2t+2)^k}.\end{aligned}$$

Next, $S_3(k)$ would be the sum of $27$ fractions (one for each cubic monic polynomial), and so on. Then $\zeta(k)=S_0(k)+S_1(k)+S_2(k)+\cdots$.

Dinesh Thakur's 2009 paper focuses on the degrees of these parts $S_d (k)$. Here, the degree of a fraction $\frac{f(t)}{g(t)}$ is defined as $\deg f-\deg g$; so for example $S_2(k)$ is the sum of a bunch of fractions of degree $-2k$. (Negative degrees are allowed, and most degrees in this problem will be negative.)

Why is understanding the degrees of $S_d (k)$ so hard? There is an obstacle that's not obvious: hidden cancellation that occurs because we are working modulo $q$.

Let's give a concrete example to show what this means. Pick $q = 3$, $d = 1$, and $k = 5$. Then

$$S_1(5)=\frac{1}{t^5}+\frac{1}{(t+1)^5}+\frac{1}{(t+2)^5}.$$

Each of the three fractions is degree $-5$ in $t$. So shouldn't $S_1(5)$ just be degree $-5$?

But it isn't. If we brute-force the calculation, we get

$$\begin{aligned}S_1(5)&=\frac{(t+1)^5(t+2)^5+t^5(t+2)^5+t^5(t+1)^5}{t^5(t+1)^5(t+2)^5}\\&=\frac{3t^{10}+30t^9+150t^8+480t^7+1070t^6+1716t^5+1970t^4+\cdots}{t^5(t+1)^5(t+2)^5}.\end{aligned}$$

This looks like a degree $10$ polynomial over a degree $15$ polynomial, so the degree still seems like $10 - 15 = -5$. But the catch is that we are working modulo $3$, which means we have to take all the remainders when dividing by $3$. The $3t^{10}$ is a multiple of $3$, so it vanishes. So do $30 t^9$, $150 t^8$, and $480 t^7$, and suddenly, the biggest terms in our numerator melt away. If you compute all the way, you find what's left over is

$$S_1(5)=\frac{\left(2t^6+2t^4+2t^2+2\right)\bmod 3}{t^5(t+1)^5(t+2)^5}.$$

For example, the $t^{10}$ term we were hoping to get in the numerator got cancelled out, because each of the three original fractions contributed one $t^{10}$, and $1+1+1\equiv 0\pmod{3}$. In fact the $t^9$, $t^8$, $t^7$ terms all cancelled too. When the dust settles, we see that $S_1(5)$ is actually of degree $6 - 15 = -9$, not degree $-5$ like we might have expected.

In what follows, we'll define the shorthand

$$ s_d (k) := - \deg S_d (k) $$

just so that we don't have to keep writing minus signs everywhere. So for example, $s_1(5) = 9$.

We've seen that controlling the combinatorics of $s_d (k)$ can be tricky. But as a reward, Thakur shows that understanding $s_d (k)$ pays in spades. His paper shows how proving results about $s_d (k)$ "quickly leads to many interesting structural facts, such as Riemann hypothesis for Carlitz-Goss zeta function, monotonicity in degree, non-vanishing and special identity classification for function field multizeta, as easy consequences".

Thakur lists three specific conjectures, which are called Hypotheses H1, H2, and H3. These remained open, and solving these conjectures is the main goal of our paper. We'll describe the three hypotheses in a moment; first, though, we'll walk through the simplest case $d = 1$.

To give a demonstration of the ideas that go into our proof, we'll show how to turn the calculation of $s_1(k)$ into a grade-school question about adding digits. We're going to need two ingredients: Taylor series from high school calculus, and Lucas' theorem. Both center around binomial coefficients, the numbers that appear in Pascal's triangle.

The binomial theorem from high school tells us that for positive integers $n$, we can expand $(1+X)^n$ to get the numbers in Pascal's triangle; that is,

$$\begin{aligned}(1+X)^0&=\binom{0}{0}&&=1\\(1+X)^1&=\binom{1}{0}+\binom{1}{1}X&&=1+X\\(1+X)^2&=\binom{2}{0}+\binom{2}{1}X+\binom{2}{2}X^2&&=1+2X+X^2\\(1+X)^3&=\binom{3}{0}+\binom{3}{1}X+\binom{3}{2}X^2+\binom{3}{3}X^3&&=1+3X+3X^2+X^3\\&\vdots\end{aligned}$$

and so on. However, it turns out that by using Taylor series from calculus, we can get an expansion like this for negative exponents too - as long as we're okay with an infinite sum rather than a finite one. The pattern looks like this:

$$\begin{aligned}(1+X)^{-1}&=\binom{0}{0}-\binom{1}{0}X+\binom{2}{0}X^2-\binom{3}{0}X^3+\cdots&&=1-X+X^2-X^3+\cdots\\(1+X)^{-2}&=\binom{1}{1}-\binom{2}{1}X+\binom{3}{1}X^2-\binom{4}{1}X^3+\cdots&&=1-2X+3X^2-4X^3+\cdots\\(1+X)^{-3}&=\binom{2}{2}-\binom{3}{2}X+\binom{4}{2}X^2-\binom{5}{2}X^3+\cdots&&=1-3X+6X^2-10X^3+\cdots\\&\vdots\end{aligned}$$

and in general,

$$\frac{1}{(1+X)^n}=\binom{n-1}{n-1}-\binom{n}{n-1}X+\binom{n+1}{n-1}X^2-\binom{n+2}{n-1}X^3+\cdots.$$

Since we're going to be taking modulo $q$ so often, it'll be helpful to know when binomial coefficients are divisible by $q$. Lucas' theorem provides the answer to this: it turns out the answer is closely tied to the digits in base $q$.

Lucas' theorem. Let $n \geq k \geq 0$ be integers and $q$ a prime. Then $\binom{n}{k}$ is divisible by $q$ if and only if adding $(n-k) + k$ in base $q$ has at least one carry.

For example, let $q = 3$. The addition $5 + 2 = 7$ in base $3$ has a carry:

$$(12)_3+(2)_3=(21)_3\quad\Longrightarrow\quad\binom{7}{2}=21\text{ is divisible by }3.$$

Whereas the addition $5 + 3 = 8$ in base $3$ has no carries:

$$(12)_3+(10)_3=(22)_3\quad\Longrightarrow\quad\binom{8}{3}=56\text{ is not divisible by }3.$$

Let's go back to our example of $s_1(5) = 9$ (for $q=3$). Our Taylor series is

$$\begin{aligned}(1+X)^{-5}&=1-5X+15X^2-35X^3+70X^4+\cdots\\&=\binom{4}{4}-\binom{5}{4}X+\binom{6}{4}X^2-\binom{7}{4}X^3+\binom{8}{4}X^4-\cdots.\end{aligned}$$

Choosing $X = t^{-1}$ and $X = 2t^{-1}$ gives

$$\begin{aligned}\frac{1}{(t+1)^5}&=\frac{t^{-5}}{(1+t^{-1})^5}=t^{-5}-5t^{-6}+15t^{-7}-35t^{-8}+\cdots\\\frac{1}{(t+2)^5}&=\frac{t^{-5}}{(1+2t^{-1})^5}=t^{-5}-10t^{-6}+60t^{-7}-280t^{-8}+\cdots\end{aligned}$$

If we just add these numerically, we get

$$\begin{aligned}S_1(5)&=\frac{1}{t^5}+\frac{1}{(t+1)^5}+\frac{1}{(t+2)^5}\\&=3t^{-5}-15t^{-6}+75t^{-7}-315t^{-8}+1190t^{-9}-4158t^{-10}+13650t^{-11}+\cdots.\end{aligned}$$

As we expect, when we take modulo $3$, the first four terms melt away and the first term not divisible by $3$ is $1190t^{-9}\equiv 2t^{-9}\pmod{3}$, confirming that $s_1(5) = 9$ again.

But this time around, the coefficients come from a predictable formula. If we retrace our steps, the pattern is:

$$\begin{aligned}S_1(5)&=3t^{-5}-\binom{5}{4}(2^1+1)t^{-6}+\binom{6}{4}(2^2+1)t^{-7}\\&\quad-\binom{7}{4}(2^3+1)t^{-8}+\binom{8}{4}(2^4+1)t^{-9}-\cdots.\end{aligned}$$

In general the coefficient for $t^{-n}$ is exactly $\pm\binom{n-1}{4}\left(2^{n-5}+1\right)$ for $n > 5$. For example, the critical coefficient for $t^-9$ came from $\binom{8}{4}\times(2^4+1)=70\times(16+1)=1190$.

So $s_1(5)$ is the smallest integer $n > 5$ such that (i) $2^{n-5}+1$ is not divisible by $3$, and (ii) $\binom{n-1}{4}$ is not divisible by $3$. It's easy to see (i) happens exactly when $n$ is odd, and (ii) is controlled by Lucas' theorem: it means adding $(n-5)+4$ in base $3$ should have no carries. Thus, determining $s_1(5)$ for $q = 3$ amounts to looking for an integer $n$ such that

• $n - 5$ is a positive even number; and
• adding $(n-5)+4$ in base $3$ produces no carries.

Suddenly all the polynomials are gone! All that's left is a problem about carry-free addition.

There's nothing special about $5$ here, or the prime $q=3$. By repeating the same argument, we find that $s_1(k)$ is the smallest integer $n > k$ such that

• $n - k$ is a positive multiple of $q-1$; and
• the addition $(n-k) + (k-1)$ has no carries in base $q$.

And thus, we've figured out how to work with $s_1(k)$ in terms of grade-school addition.

The situation of $s_d (k)$ for $d > 1$ is more complicated. But the underlying strategy for controlling these numbers is similar: use Lucas' theorem and Taylor series to turn the problem into a grade-school addition question, and then analyze the digits. Using these techniques, we proved the three hypotheses H1, H2, and H3. We describe now roughly what they say.

Hypothesis H1 is the most complicated to state of the three hypotheses. It involves something that we'll call a stone placement puzzle in this post.

In a stone placement puzzle there's a finite rectangular grid with the triangle in the lower-right removed, as in the figure below. The puzzle specifies a label from $0$ to $q-1$ for each column. Then the stone placement asks us to place stones within all the cells, such that

• The total number of stones in each column matches the label.
• Every NE-SW diagonal has at most $q-1$ stones in it.

In addition, every cell has a point value given by a certain formula in the paper; one scores that point value for each stone in that cell. The goal of the puzzle is to find legal placements of stones minimizing the total score (i.e. lower scores are better).

Hypothesis H1 says that calculating $s_d (k)$ corresponds exactly with finding the best solution to the stone placement puzzle. To be more precise:

Hypothesis H1. In every stone placement puzzle, the best possible score $C$ is obtained by exactly one placement of stones (i.e. there are no ties). Moreover, $s_d (k) = d k + C$.

In our paper, we not only prove H1, but also give an algorithm for finding the optimal placement; it's referred to as a greedy algorithm. The greedy algorithm can be described succinctly as follows: fill in the stones going from the rightmost column to the leftmost column, and within each column, place the stones in the lowest row they fit in.

Hypothesis H2 concerns a certain recursive way to write $S_d (k)$. Later on in this post, we'll show the full technical statement of H2. But it's actually the following corollary of H2 that is more natural:

(Corollary of) Hypothesis H2. For all $d \ge 1$, $$s_d(k)=\underbrace{s_1(k)+s_1\bigl(s_1(k)\bigr)+s_1\bigl(s_1(s_1(k))\bigr)+\cdots}_{d\text{ summands}}.$$

So, H2 can be interpreted as saying that computing $s_d (k)$ boils down to calculating $s_1$ over and over.

Hypothesis H3 is the simplest to state. It says that the degrees generally go up as $k$ goes up:

Hypothesis H3. If $q$ does not divide $k$, then $s_d (k) < s_d (k+1)$.

Having AxiomProver automatically formalize the results in this paper was actually a bumpier ride than we would've liked. In other AxiomProver projects, the process was sometimes truly fire-and-forget: type in the problem statement into the machine, and watch a Lean proof appear. But this was not such a project.

In this project, the problem statement and solution have a lot of moving parts. This alone is already a cause for concern, because the more components you have, the more things can go wrong. However, one intermediate step was particularly troublesome: the usage of Sheats' 1997 uniqueness theorem in the proofs of H2 and H3. Unlike other theorems we quoted (such as Lucas' theorem), Sheats' theorem doesn't appear in Mathlib and can't be easily re-proved from axioms.

To overcome this, we split the main task into four subtasks: one each called H1, H2, H3, together with a setup subtask called Lem41 (proving what is now Lemma 4.1 in the most recent paper). Each task was written with clear separation of concerns in mind; this way, each subtask could be resolved in isolation. Sheats' uniqueness theorem then serves as the bridge from Lem41 to the main goal. Here is the figure from our paper showing how we structured the plan.

This subdivision made it possible to create much more modular subtasks that would not get caught up, say, trying to re-prove Sheats' uniqueness theorem from scratch. For example, before division, the task description for H2 looked like this:

Let $q$ be a prime.  Let $A := \mathbb{F}_q[t]$ and for integers $d\geq 0$, write $A_d^+$ for the monic polynomials in $A$ of degree $d$.  Define $S_d(k) \coloneq \sum_{a\in A_d^+}\frac{1}{a^k}\in \mathbb{F}_q(t)$ and $s_d(k) = -\deg_t S_d(k) \ge 0$ for each integer $k \ge 0$.

Fix integers $k \ge 0$ and $d \ge 1$.  Consider all $j \geq 0$ satisfying $(q-1) \mid j$ and $\binom{s_1(k)+j-1}{k-1}\not\equiv 0\pmod q$.  Prove that for such $j$, the function $s_{d-1}(s_1(k)+j)+s_1(k)+j$ has a unique minimum at $j = 0$.

However, after the subdivision, we could present the task in a way that didn't even reference polynomials, which made it much easier to prove. Here was the final form of the H2 subtask:

Let $q$ be a prime.  If $d \ge 1$ and $k > 0$ are integers, we define $\mathcal{T}_{d,k-1}$ to be the set of $d$-tuples $(m_1, \dots, m_d)$ such that

(1) $m_i > 0$ for all $1 \le i \le d$
(2) $q-1$ divides $m_i$ for all $1 \le i \le d$
(3) the addition $(k-1) + m_1 + \dots + m_d$ has no carries in base $q$.

Then, define $s_d(k) = dk + \min(m_1 + 2m_2 + \dots + dm_d)$ where the minimum is taken over all tuples in $\mathcal{T}_{d,k-1}$.  (The set $\mathcal{T}_{d,k-1}$ is always nonempty, so this minimum exists: for instance, take $m_i = (q-1) q^{e_i}$ for distinct exponents $e_i$ large enough that the digits of $k-1$ in those positions are zero.)

Fix integers $d > 1$ and $k > 0$.  Consider all integers $j \ge 0$ such that $q-1$ divides $j$ and $\binom{s_1(k) + j-1}{k-1}$ is not divisible by $q$.  Among all such $j$, show that the quantity $s_{d-1}(s_1(k)+j) + s_1(k)+j$ is minimized uniquely at $j = 0$.

In some sense, our subtask division is a tiny example of what the Lean community more broadly calls a blueprint. As the tasks we provide AxiomProver become increasingly ambitious, moving away from mostly-standalone 20-page papers to entire frameworks and libraries, we expect that planning like this will be increasingly critical.

• Paper: "Thakur's Hypotheses on Power Sums over $\mathbb{F}_q[t]$", by Evan Chen and Ken Ono
• arXiv: https://arxiv.org/abs/2606.16239
• Code: https://github.com/AxiomMath/zeta-h123