The Purpose of the Object

This story starts from a problem that we saw back in December 2025, back when AxiomProver was attempting the 2025 Putnam exam. To describe what the Putnam problem is about, we'll start by considering the $4! = 24$ permutations of $(1,2,3,4)$. For such a permutation $\left( a_{1},a_{2},a_{3},a_{4} \right)$, we look at the $3$ pairs of adjacent elements and see which one is larger. There are $2^{3} = 8$ possibilities, which we list in the table below.

The Putnam 2025 problem replaces $4$ with any $n \geq 2$ and asks which of the $2^{n - 1}$ rows have the largest counts. The answer is what you'd guess from the table: the two rows with zigzag permutations (meaning the numbers alternate going up and down) are always the two largest rows, for every choice of $n$.

This naturally raises the question: what is that maximum $E_{n}$? (For example, the above table shows $E_{4} = 5$.) This problem dates all the way back to 1881, when Désiré André showed that the answer is exactly $n!$ times the $x^{n}$ coefficient in the Taylor series of $\sec(x) + \tan(x)$. That number $E_{n}$ is today called the zigzag number, Euler zigzag number, or up/down number; the first few zigzag numbers are given by$$E_{1} = E_{2} = 1,\, E_{3} = 2,\, E_{4} = 5,\, E_{5} = 16,\, E_{6} = 61,\, E_{7} = 272,\, E_{8} = 1385,\ldots$$

These numbers turn out to show up in many other places in mathematics. For example, Bernoulli saw the same sequence appear in 1742 (see Figure 1).

Coming back to present-day 2026, the zigzag numbers appeared yet again in a number-theoretic paper by Amdeberhan, Ono, and Singh. This time, however, they arose in connection with the theory of partitions.

A partition $\lambda$ of a positive integer $n$ is just an unordered way to write $n$ as the sum of one or more positive integers. For example, there are five possible partitions for $n = 4$: namely, $4$, $3 + 1$, $2 + 2$, $2 + 1 + 1$, and $1 + 1 + 1 + 1$. Partitions have appeared in past Axiom work as well, for example in our July 2026 post The Address Before the Room.

One of the results that came out of the Amdeberhan-Ono-Singh paper was a complicated identity tying different zigzag numbers together. For each partition $\lambda$ of $n$, they had stumbled upon the quantity$$P(\lambda) ≔ (2n)!\prod_{k = 1}^{n}\frac{1}{m_{k}(\lambda)!}\left( \frac{E_{2k - 1}}{(2k)!} \right)^{m_k(\lambda)}$$where $m_{k}(\lambda)$ is the number of times $k$ appears in the partition $\lambda$. One of the consequences of their work was that if you add up all the $P(\lambda)$, across all possible partitions $\lambda$ of $n$, you actually end up with just $E_{2n}$:$$\sum_{\lambda}P(\lambda) = E_{2n}.$$

Because of André's counting interpretation of $E_{2n}$ as zigzag permutations of $\left\{ 1,2,\ldots,2n \right\}$, it's natural to wonder whether $P(\lambda)$ might also have an interpretation that explains this sum.

In 2026, Amdeberhan, Shareshian, and Stanley found that there was indeed a way to interpret $P(\lambda)$, using the concept of records. We'll explain their interpretation now.

From now on, we'll fix the convention that we consider permutations $w = a_{1}a_{2}\ldots a_{2n}$ of $\left\{ 1,2,\ldots,2n \right\}$ for which $$a_{1} > a_{2} < a_{3} > a_{4} < \ldots.$$

(For experts: we choose the convention of down-up rather than up-down from now on.) Then a record refers to an entry of $w$ which is strictly larger than all the earlier entries when we read from left to right. For example, if $n = 5$ and we take the example$$w = 7\, 2\, 5\, 4\, 8\, 3\, 10\, 6\, 9\, 1$$ then the records are at $7$, $8$, and $10$.

To define the record composition of $w$, suppose we cut $w$ just before every record other than the first. This divides $w$ into several blocks. Because $w$ was down-up, these blocks necessarily all have even length, and sum to $2n$. The ordered sequence of half the block lengths is called the record composition of $w$, which we call $\operatorname{rc}(w)$. In the example above, the cuts would be placed at $$w = 7\, 2\, 5\, 4~|~8\, 3~|~10\, 6\, 9\, 1$$which divides $w$ into blocks of length $4 + 2 + 4$, so we write$$\operatorname{rc}(w) = (2,1,2).$$

For a given record composition $\alpha$, we let $N(\alpha)$ denote the number of zigzag permutations with that record composition. Then the result from Amdeberhan-Shareshian-Stanley goes as follows.

Theorem 1 (Amdeberhan-Shareshian-Stanley, 2026): The quantity $P(\lambda)$ defined by the formula earlier counts the number of zigzag permutations $w$ whose record composition $\operatorname{rc}(w)$ rearranges to the partition $\lambda$, ignoring the order of $\operatorname{rc}(w)$. That is,$$P(\lambda) = \sum_{\alpha\text{ rearranges to }\lambda}N(\alpha).$$

Theorem 1 thus gives a simple explanation for why $\sum_{\lambda}P(\lambda) = E_{2n}$, by identifying the zigzag counting problem with answer $P(\lambda)$.

(Notice the interesting reversal in the history: we started with an answer $P(\lambda)$ pulled out of a number theory paper, and had to figure out what question it was answering! This is a bit like the dilemma faced in The Hitchhiker's Guide to the Galaxy, where it is discovered the Ultimate Answer is $42$, but the Ultimate Question remains unknown.)

To summarize, Theorem 1 shows how the formula $P(\lambda)$ is actually the sum of all $N(\alpha)$ where $\alpha$ rearranges to $\lambda$. However, this raises the question of what $N(\alpha)$ itself is, and Amdeberhan-Shareshian-Stanley propose this as an open problem.

To make this concrete, let's draw a picture for $n = 4$. It turns out $E_{8} = 1385$, so there will be $1385$ possible zigzag permutations in play. As we saw, there are five partitions $\lambda$ of $n = 4$, and if one applies Theorem 1 and carefully evaluates the complicated formula, it will spit out five numbers: $$\begin{aligned}P(4) & = 272 \\P(3 + 1) & = 448 \\P(2 + 2) & = 140 \\P(2 + 1 + 1) & = 420 \\P(1 + 1 + 1 + 1) & = 105.\end{aligned}$$

But there are $8$ possible record compositions, which we've grouped together into the figure shown below.

We see we get $N(4)$, $N(2,2)$, and $N(1,1,1,1)$ directly from Theorem 1, because the sum in Theorem 1 only has one term. But what about the others? Theorem 1 is only precise enough to tell us the sums $N(3,1) + N(1,3) = 448$ and $N(2,1,1) + N(1,2,1) + N(1,1,2) = 420$, but it doesn't tell us how to refine that information further. This refinement is the problem proposed by Amdeberhan-Shareshian-Stanley.

Our paper answers the problem of Amdeberhan-Shareshian-Stanley by giving a full formula for every $N(\alpha)$. Actually there are three equivalent formulas stated in our paper; the following one is easiest to understand.

Theorem 2. If $\alpha = \left( \alpha_{1},\ldots,\alpha_{\ell} \right)$ then $N(\alpha)$ is given exactly by the formula$$N(\alpha) = \prod_{j = 1}^{\ell}\binom{2\left( \alpha_{1} + \ldots + \alpha_{j} \right) - 1}{2\alpha_{j} - 1}E_{2\alpha_{j} - 1}. $$

For example, to replicate the $N(3,1)$ and $N(1,3)$ in the example, one would compute $$\begin{aligned}N(3,1) & = \binom{5}{5}E_{5} \cdot \binom{7}{1}E_{1} = (1 \cdot 16) \cdot (7 \cdot 1) = 112, \\N(1,3) & = \binom{1}{1}E_{1} \cdot \binom{7}{5}E_{5} = (1 \cdot 1) \cdot (21 \cdot 16) = 336.\end{aligned}$$

This time, the AxiomProver story will be pretty boring. We gave it the theorem statement we wanted, actually in three different forms, and asked AxiomProver to prove them all (by itself, with no guidance or informal proof). It succeeded. The end.

Actually the hardest part of the formalization was not the combinatorial proof itself, but one of those three forms. To explain the context, Amdeberhan-Shareshian-Stanley had provided an alternate version of Theorem 1 where the $P(\lambda)$ appear as the coefficients of a sequence of commutative symmetric functions which they called a sprout sequence. Thus, when we constructed our Theorem 2, one of the forms interpreted $N(\alpha)$ as the coefficients of a symmetric function, in analogy to the sprout sequence interpretation of Theorem 1.

The difference was that for us, because $N(\alpha)$ is sensitive to order (e.g. $N(3,1) = 112 \neq 336 = N(1,3)$), we needed to use noncommutative symmetric functions instead of commutative ones. We'll give the statement here just to show how different this variant looks, although defining the terms is beyond the scope of this post.

Theorem 2, noncommutative symmetric function form. Let $\Psi^{\alpha}$ denote the noncommutative power sums of the first kind associated to an ordered sequence $\left( \alpha_{1},\ldots,\alpha_{\ell} \right)$. Then for every positive integer $n$, the noncommutative symmetric function $$\sum_{\alpha_{1} + \ldots + \alpha_{\ell} = n}N(\alpha)\Psi^{\alpha}$$coincides with the canonical noncommutative lift of the sprout sequence with seed $\sec(\sqrt{t})$ introduced by Amdeberhan-Shareshian-Stanley. (Here the sum is across all compositions $\alpha$ with sum $n$.)

If one actually learns the definitions of all the big words used in this version of Theorem 2, it is pretty straightforward to show it is actually saying the same thing as the earlier version. However, if one examines the solution.lean produced by AxiomProver, most of the lines of code are actually dedicated to setting up the algebraic scaffolding needed to show this equivalence. So this is another case where the relative difficulty for a formalizer is quite different from the relative difficulty for human mathematicians.

• Paper: "Record compositions of alternating permutations and noncommutative symmetric functions", by Evan Chen, Michal Mogielnicki, and Ken Ono
• arXiv: https://arxiv.org/abs/2607.12873
• Code: https://github.com/AxiomMath/record-compositions