Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns (experimental)
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Is every odd number a sum of k primes? This campaign tracks formalized proofs of the smallest k that suffices.
Schnirelmann (1930) showed some finite k works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved k=5 unconditionally. Helfgott (2013) proved that every odd number greater than 5 is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: 27 is neither prime nor 2 + prime.
Schoolbook matrix multiplication takes n3 operations. The exponent ω is the infimum of all τ such that two n×n matrices can be multiplied in O(nτ) arithmetic operations; trivially ω≥2, and ω=2 is conjectured but open.
Strassen gave the first nontrivial bound, ω<2.81, in 1969, and introduced the laser method in 1986 to reach ω<2.48. Coppersmith and Winograd's 1990 bound of 2.376 stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached ω<2.371339 in 2025, and the current record is ω<2.371177, from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Primal-Dual Online Algorithms II: Finite LP Duality and Complementary SlacknessTextbook
## Motivation
Almost every competitive online algorithm built by the primal-dual method rests on the same two facts about a pair of linear programs. The first is *weak duality*: any feasible solution of the dual is a lower bound on any feasible solution of the primal. The second is *complementary slackness*: if a feasible primal-dual pair satisfies a local, per-coordinate tightness condition, the pair is optimal — and if it satisfies that condition only up to factors $\alpha$ and $\beta$, the primal is within $\alpha\beta$ of optimal.
The second fact in its approximate form is the engine of the whole method. An online algorithm cannot compute an optimum; what it can do is maintain a primal solution and a dual solution side by side so that each new request preserves an approximate tightness invariant. The approximate complementary slackness theorem then converts that local invariant into a global competitive ratio, with no reference to the optimum at all. Chapter 2 of Buchbinder's thesis states it as the background result on which the rest of the work is built.
## Setting
Fix finite index types $I$ (primal variables) and $J$ (primal constraints), a matrix $A : I \times J \to \mathbb{R}$, a cost vector $c : I \to \mathbb{R}$ and a right-hand side $b : J \to \mathbb{R}$. The covering primal and packing dual are
$$(P)\quad \min \sum_{i} c_i x_i \ \text{ s.t. } \ \sum_{i} A_{ij} x_i \ \ge\ b_j \ \ (\forall j), \qquad x \ge 0,$$
$$(D)\quad \max \sum_{j} b_j y_j \ \text{ s.t. } \ \sum_{j} A_{ij} y_j \ \le\ c_i \ \ (\forall i), \qquad y \ge 0.$$
Note the index convention: $A_{ij}$ carries the primal-variable index *first*, so the primal constraint indexed by $j$ sums over $i$ and the dual constraint indexed by $i$ sums over $j$.
Given $\alpha, \beta \ge 1$, the pair $(x,y)$ satisfies **approximate complementary slackness** when
- primal side: for every $i$ with $x_i > 0$, $\quad c_i/\alpha \ \le\ \sum_j A_{ij} y_j \ \le\ c_i$;
- dual side: for every $j$ with $y_j > 0$, $\quad b_j \ \le\ \sum_i A_{ij} x_i \ \le\ \beta\, b_j$.
## Formalization targets
### Goal — approximate complementary slackness
For a primal-feasible $x$, a dual-feasible $y$, and $\alpha,\beta \ge 1$ satisfying the two conditions above,
$$\sum_{i} c_i x_i \ \le\ \alpha\beta \sum_{j} b_j y_j .$$
Taking $\alpha = \beta = 1$ recovers exact complementary slackness and hence optimality of both members of the pair. The goal is stated with the source's hypotheses, including the two-sided bounds, rather than the weakest hypotheses that make the inequality go through; a separate item records the minimal-hypothesis strengthening.
### Weak duality
$$\sum_j b_j y_j \ \le\ \sum_i c_i x_i \quad \text{for every feasible } x \text{ and } y,$$
with no nonnegativity assumption on $A$, $b$ or $c$ beyond feasibility itself.
### Strong duality — imported, not reproved
Strong duality is **not** proved in this mission. The platform already carries `LinearOptimization.lp_strong_duality`, proved in this exact environment, for linear programs in Bertsimas–Tsitsiklis general form over `Fin`-indexed data. This mission's contribution is an *adapter*: from a primal optimum of $(P)$, produce a dual optimum of $(D)$ of equal value, for `Fin`-indexed instances. Reference items point at the imported theorem, its dual construction, and the dual-of-dual identity.
The biconditional — a dual optimum exists *if and only if* a primal optimum does — is deliberately left **open**. Weak duality does not derive the existence of a primal optimum from the existence of a dual one; the reverse implication needs strong duality applied to the dual program together with the dual-of-dual identity, and that reduction is not yet compiled. It is offered as a parallel target rather than claimed as established.
## Significance
This mission is the foundation of the series. Every later mission — set cover, ski rental, and the online covering and packing problems that follow — states its approximation or competitiveness result as an instance of approximate complementary slackness. Formalizing it once, over arbitrary finite index types, is what makes the later missions short.
It also fills a real gap. Mathlib currently has no linear-programming duality: four separate attempts were closed unmerged. Approximate $(\alpha,\beta)$ complementary slackness appears not to be formalized in any public library, so the goal theorem is, as far as we can determine, first of its kind.
## Difficulty
The goal is a summation argument, not a deep theorem: the work is in handling the per-coordinate case split on $x_i > 0$ versus $x_i = 0$ and in interchanging a double sum. Three mechanical milestones isolate exactly those steps. The strong-duality adapter is the hard item, because it must reconcile two different presentations of the same program — index types, matrix orientation, and bundling all differ between our definitions and the imported theorem's.
## Formalization scope
Definitions cover §2.1 of the source. Four distinct notions of "the program has a finite optimum" are separated on purpose — attained optimum, nonempty feasible set, bounded objective, and the conjunction — because the source's informal word "bounded" conflates them. The definitions are stated over arbitrary finite index types; the strong-duality items are stated only for `Fin`, because that is the only index type for which the imported dependency path exists.
## Selected references
- Niv Buchbinder, *Designing Competitive Online Algorithms via a Primal-Dual Approach*, PhD thesis, Tel Aviv University, 2008, §2.1, pp. 7–9. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
- Dimitris Bertsimas and John N. Tsitsiklis, *Introduction to Linear Optimization*, Athena Scientific, 1997 — the general form used by the imported strong-duality theorem.
Magic Squares II: MacMahon's Enumeration of Order-Three Semi-Magic SquaresResearch Paper
## Motivation
This is the second mission in the magic-squares formalization programme, and it
takes up the case the first one deliberately left open.
Counting **semi-magic squares** — arrays of nonnegative integers whose rows and
columns all share a common line sum, with the diagonals unconstrained — is the
"honest" version of the enumeration problem. For order three the *magic* count
$M_{3}(t)$ (mission I) is only a **quasi-polynomial**: it vanishes unless
$3\mid t$ and equals $2e^{2}+2e+1$ on $t=3e$. The **semi-magic** count $H_{3}(t)$
has no such periodicity. MacMahon computed it in 1915:
$$H_{3}(t)\;=\;3\binom{t+3}{4}+\binom{t+2}{2}.$$
It is an honest polynomial in $t$ of degree $4=(3-1)^{2}$, and that degree is
not an accident: Ehrhart and Stanley proved that for every order $n$ the
function $H_{n}(t)$ is a **polynomial** of degree $(n-1)^{2}$ satisfying the
reciprocity law $H_{n}(-n-t)=(-1)^{n-1}H_{n}(t)$. The order-three formula above
is the smallest nontrivial instance of that theorem, and the only one small
enough that every step of the derivation can still be exhibited explicitly.
So this mission is the natural companion to mission I: same objects, same
platform vocabulary, but the counting step is genuinely harder — the parameter
space is four-dimensional rather than two, and the parametrization is *not*
injective until it is normalized.
## Setting
Fix $n$ and a line sum $t$. A **square** of order $n$ is an $n\times n$ array
$M$ of nonnegative integers.
* $M$ is **semi-magic** with line sum $t$ if every row and every column sums to
$t$. No condition is imposed on the two diagonals, and entries need not be
distinct.
* $H_{n}(t)$ is the number of such squares. Every entry is at most $t$, so
$H_{n}(t)$ is the cardinality of a finite set.
For $n=3$ the whole family is governed by the six permutation matrices. Split
them into the three **even** ones — the identity and the two $3$-cycles — whose
supports are the transversals
$$D=\{00,11,22\},\qquad E=\{01,12,20\},\qquad F=\{02,10,21\},$$
and the three **odd** ones — the transpositions — with supports
$$A=\{00,12,21\},\qquad B=\{02,11,20\},\qquad C=\{01,10,22\}.$$
Adding them with multiplicities $u,v,w$ (even) and $x,y,z$ (odd) gives
$$M=\begin{pmatrix} u+x & v+z & w+y\\ w+z & u+y & v+x\\ v+y & w+x & u+z\end{pmatrix},$$
whose six line sums all equal $u+v+w+x+y+z$; so this is a semi-magic square of
line sum $t$ whenever the multiplicities sum to $t$.
## Formalization targets
### Goal — MacMahon's semi-magic count
$$H_{3}(t)\;=\;3\binom{t+3}{4}+\binom{t+2}{2}\qquad\text{for every }t\ge 0 .$$
This is the goal because it is the weakest statement that still pins down the
answer: it asserts the shape of $H_{3}$ without naming the parametrization, and
it survives verbatim as the $n=3$ case of Stanley's theorem that $H_{n}$ is a
polynomial of degree $(n-1)^{2}$.
### The route
1. **Canonical decomposition** (`sm3_canonical`). Every $3\times3$ semi-magic
square arises from the display above, and the representation becomes unique
after normalizing: put $u=\min D$, $v=\min E$, $w=\min F$, subtract the
corresponding even permutation matrices, and the residual odd multiplicities
satisfy $\min(x,y,z)=0$. The normalization is necessary — without it the
single relation
$$D+E+F=A+B+C\;(=J)$$
identifies distinct $6$-tuples — and it is exactly what makes the count a
*partition* rather than an inclusion–exclusion.
2. **Bijection** (`sm3_bij`). The map from normalized coefficient vectors to
semi-magic squares is a bijection, so $H_{3}(t)=\mathrm{sm3Count}(t)$.
3. **Stars and bars** (`comps_card`). The number of $k$-tuples of nonnegative
integers summing to $n$ is $\binom{n+k-1}{n}$; the case $k=5$ is what the
count needs.
4. **Evaluating the parameter count** (`sm3_params_card`). Partitioning the
normalized vectors according to the *first* zero among $(x,y,z)$ writes
$\mathrm{sm3Count}(t)$ as
$$\binom{t+4}{4}+\binom{t+3}{4}+\binom{t+2}{4},$$
which collapses to $3\binom{t+3}{4}+\binom{t+2}{2}$ by two applications of
Pascal's identity.
## Significance
*The result itself.* $H_{3}$ is the $n=3$ case of a theorem that launched a
subject: Stanley's proof that $H_{n}(t)$ counts lattice points in the
Birkhoff polytope $t\cdot B_{n}$ makes $H_{n}$ an Ehrhart polynomial, and the
order-three formula is the first nontrivial value of it. Beck, Cohen, Cuomo and
Gribelyuk ([*Amer. Math. Monthly* **110** (2003),
707--717](https://arxiv.org/abs/math/0201013)) revisited exactly this
computation on the way to their quasi-polynomial theorem for the *magic* counts,
and Beck and Zaslavsky later pushed the same technique to the panmagic and
symmetric refinements. Getting $H_{3}$ machine-checked therefore validates the
whole hierarchy at its base.
*Formalizing it.* Nothing here is open; the mathematics is a century old. What
is missing is the formalized artifact, and the difficulty is concentrated in two
places that are formalization difficulties rather than mathematical ones.
First, **surjectivity of the permutation-matrix parametrization**. The usual
proof quotes Birkhoff–von Neumann, which in turn needs Hall's marriage theorem.
For order three one can instead do it by hand: subtract the three even
transversal minima and show that the residual satisfies $M_{01}=M_{10}$. That
last step is a six-case argument in linear arithmetic — if $b=M_{01}>c=M_{10}$
then each of the three ways for the transversal $E$ to have minimum zero forces
$c\ge b$ — and it is precisely the kind of step that is invisible on paper and
must be made explicit in a proof assistant.
Second, **the counting step**. The parameter set is a filtered finset of
functions `Fin 6 → Fin (t+1)`, while the formula is stated with binomial
coefficients over $\mathbb{N}$. Connecting them requires stars-and-bars, proved
from scratch (by induction on the number of parts plus the hockey-stick
identity), because the available library results count *sub-multisets* rather
than *compositions*. And the final collapse to MacMahon's form is a chain of
Pascal identities that must be applied in the right order to stay inside
$\mathbb{N}$, where subtraction is truncated.
## Difficulty
Two traps deserve to be named.
*Uniqueness needs the normalization.* The representation by six multiplicities
is *not* injective: $J=D+E+F=A+B+C$. Any formalization that counts $6$-tuples
directly will overcount, and the correction is not a subtraction but a choice of
canonical representative. Deciding "first zero among $(x,y,z)$" is what turns
the count into a genuine partition.
*Truncated subtraction.* The decomposition is expressed over $\mathbb{N}$, so
every identity — in particular the recovery of the multiplicities from a square
— must be stated with the admissibility inequalities as explicit hypotheses. A
truncated subtraction is only correct because normalization forbids the
truncation, and that side condition has to be discharged rather than assumed.
## Formalization scope
* Squares are indexed by `Fin n`; `semiMagicCount n t` is the cardinality of a
finset of arrays over `Fin (t+1)` — lossless, since every entry is at most
$t$.
* The parametrization and its normalization are defined over $\mathbb{N}$ with
truncated subtraction where necessary.
* Trivializing formalizations are ruled out. The goal is not a statement about a
hardcoded small $t$, nor about a finset declared to have the right
cardinality: the count must be *derived*, by an explicit bijection followed by
an explicit evaluation of a finite sum.
* Reusable beyond this mission: the canonical decomposition of $3\times3$
semi-magic squares (equivalently, the toric description of the order-three
Birkhoff polytope with its single relation), the stars-and-bars lemma for
compositions into any number of parts, and the order-three counts themselves.
## Selected references
- P. A. MacMahon, *Combinatory Analysis*, Vol. II, Cambridge University Press, 1916 (the $H_3$ formula dates to his 1915 work).
- M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, *The number of "magic" squares, cubes and hypercubes*, Amer. Math. Monthly **110** (2003), 707--717. <https://arxiv.org/abs/math/0201013>
- M. Beck and T. Zaslavsky, *Six little squares and how their numbers grow*, J. Combin. Theory Ser. A **113** (2006). <https://arxiv.org/abs/math/0502370>
- R. P. Stanley, *Enumerative Combinatorics*, Vol. I, 2nd ed., Cambridge University Press, 2012 (Ehrhart theory and reciprocity for $H_n$).
Cannon-Floyd-Parry: tree diagrams and the normal form for Thompson's group FTextbook
## Why tree diagrams
**Thompson's group $F$** is a finitely presented group of piecewise-linear homeomorphisms of the
unit interval that has served since the 1960s as a standard supply of counterexamples in
combinatorial group theory: its commutator subgroup is simple, every proper quotient of it is
abelian, it contains no free subgroup of rank two, it is not elementary amenable, and whether it
is amenable is a question Cannon, Floyd and Parry report as having been raised by Geoghegan in
1979 and still open when they wrote
([CFP96](https://doi.org/10.5169/seals-87877), §4 and p. 227).
Almost nothing about $F$ is computed directly from that analytic definition. What makes the group
tractable is a combinatorial calculus: each element is encoded by a pair of finite binary trees,
and multiplication becomes a cancellation between trees. Cannon, Floyd and Parry credit the
device to Brown and devote §2 of their notes to it; everything later in those notes that requires
a computation — the two presentations of §3, the normal subgroup lattice of §4, the treatment of
Thompson's group $T$ in §5 — runs through it.
This mission formalizes that calculus and the normal form it yields.
## Setting
A real number is **dyadic** when it has the form $m/2^k$ with $m$ an integer and $k$ a
nonnegative integer. **Thompson's group $F$** consists of the increasing homeomorphisms of
$[0,1]$ that are piecewise linear with finitely many breakpoints, all breakpoints dyadic and
every slope an integer power of $2$, under composition. Two of its elements are
$$A(x) = \begin{cases} x/2 & 0 \le x \le \tfrac12\\ x - \tfrac14 & \tfrac12 \le x \le \tfrac34\\
2x-1 & \tfrac34 \le x \le 1\end{cases} \qquad
B(x) = \begin{cases} x & 0 \le x \le \tfrac12\\ x/2 + \tfrac14 & \tfrac12 \le x \le \tfrac34\\
x - \tfrac18 & \tfrac34 \le x \le \tfrac78\\ 2x-1 & \tfrac78 \le x \le 1,\end{cases}$$
and from them come $X_0 = A$ and $X_n = A^{-(n-1)} B A^{n-1}$ for $n \ge 1$, so that
$X_1 = B$.
A **standard dyadic interval** is one of the form $[a/2^n, (a+1)/2^n]$ with $a$ and $n$
nonnegative integers and $a+1 \le 2^n$. A partition $0 = x_0 < \cdots < x_m = 1$ of $[0,1]$ is a
**standard dyadic partition** when every $[x_{i-1}, x_i]$ is a standard dyadic interval.
An **ordered rooted binary tree** is a finite tree in which each vertex has either no children or
an ordered left child and right child. Its childless vertices are its **leaves**, which carry a
canonical left-to-right order; its **right side** is the path from the root always taking the
right child; a **caret** is a vertex with its two children. Assigning $[0,1]$ to the root and
splitting each interval at its midpoint between the two children gives every vertex a standard
dyadic interval, and the leaves then cut out a standard dyadic partition — the sense in which
such a tree is a **$\mathcal{T}$-tree**. The **exponents** of a $\mathcal{T}$-tree are one
nonnegative integer per leaf, in order: the $k$th is the length of the longest arc of left edges
beginning at the $k$th leaf that does not reach the right side.
A **tree diagram** is an ordered pair $(R,S)$ of $\mathcal{T}$-trees with equally many leaves. An
element $f$ of $F$ **has** that diagram when $f$ is affine on each interval cut out by the leaves
of $R$ and carries those intervals, in order, onto the intervals cut out by the leaves of $S$.
Adjoining a caret to $R$ and to $S$ at the same leaf gives another diagram for the same $f$; a
diagram admitting no such reduction — no position where both trees carry a caret — is
**reduced**.
## Formalization targets
### Goal: the unique normal form
Every $f \ne 1$ in $F$ is
$$f \;=\; X_0^{b_0} X_1^{b_1} \cdots X_n^{b_n} \, X_n^{-a_n} \cdots X_1^{-a_1} X_0^{-a_0}$$
for exactly one choice of nonnegative integers $n$, $a_0, \dots, a_n$, $b_0, \dots, b_n$ subject
to two conditions: exactly one of $a_n$ and $b_n$ is nonzero, and if $a_k > 0$ and $b_k > 0$ for
some $k < n$ then $a_{k+1} > 0$ or $b_{k+1} > 0$.
It fixes no bound on $n$ and no normalization beyond those two conditions, so no later
refinement of how the exponents are presented can invalidate it.
### Along the way
The milestone list follows §2 in order: the correspondence between standard dyadic partitions
and $\mathcal{T}$-trees, the bijection between $F$ and the reduced tree diagrams, the word read
off the exponents of $(R,S)$, a criterion for a diagram to be reduced, generation by $A$ and
$B$, and closure under multiplication of the **positive** elements — those of the form
$X_0^{b_0} \cdots X_n^{b_n}$ with every exponent nonnegative.
## What it gives
A normal form is a decision procedure: two words in the generators name the same element exactly
when their normal forms agree, so the word problem for $F$ is solved by computing them. The
generation statement is what licenses treating $F$ as a two-generator group, and it is the input
to both presentations in §3. The positive elements and their closure under multiplication are
used, with the normal form, throughout §5 on Thompson's group $T$.
The §2 results this mission targets — Lemma 2.2, the correspondence between $F$ and the
reduced tree diagrams, Theorem 2.5, Corollary 2.6, Corollary-Definition 2.7 and Lemma 2.8 — are
**proved** mathematics: Cannon, Floyd and Parry are expounding material that goes back to
Thompson's unpublished notes. None of them has a machine-checked proof on this platform, and the
library contains no tree-diagram machinery to build on, so the definitions published here fix the
interface for anyone later formalizing Thompson's groups $T$ and $V$, which occupy the same notes
and are built from the same trees.
There is also a concrete dependency. The companion mission on §4 of the same paper has eleven of
its fifteen milestones machine-checked, and **all four that remain wait on this section**: Cannon,
Floyd and Parry prove their Theorem 4.1 through Corollary 2.6 and their Theorem 4.3 through the
normal form. Corollary 2.6 appears in this milestone list as the same theorem object that is open
there, so closing it here closes it there.
## Difficulty
The obvious way to attach a diagram to an element $f$ is to use the partition given by its
breakpoints. That fails twice over: the breakpoints of $f$ need not be the division points of any
$\mathcal{T}$-tree, and even when they are, their images under $f$ need not be either, since the
definition of $F$ constrains the breakpoints and slopes of $f$ and says nothing about where the
image partition sits. Both failures must be repaired by refining the partition before any tree
appears, which is why that refinement is a milestone rather than a preliminary.
Uniqueness of the reduced diagram is a difficulty of a different kind: two reduced diagrams for
the same element admit no a priori map between their trees, so they cannot be compared directly.
A third is not visible in the source. For trees with $n+1$ leaves the exponent lists always end
in $0$, so the outermost factors of the word above vanish; but the normal form demands that
exactly one of $a_n$, $b_n$ be nonzero. The two indexings differ, and a re-indexing step sits
between the theorem producing the word and the corollary stating the normal form. The paper prints
them one under the other. That step is a milestone of its own, flagged as absent from the source,
so a solver working from the paper alone is not ambushed by it.
## Formalization scope
Ordered rooted binary trees are an inductive type — a leaf, or a pair of subtrees — rather than
graphs with a root and valence conditions. Those conditions say exactly that every non-leaf vertex
has two distinguished children, so both descriptions pick out the same objects, but the inductive
type is a **reformulation** of the paper's definition and the definition bundle says so. The
infinite tree of all standard dyadic intervals is likewise never built: the subdivision of
$[0,1]$ comes from a recursion halving at each node, which turns the paper's observation that the
leaves of a $\mathcal{T}$-tree are the intervals of a standard dyadic partition from something
given into something proved.
$F$ is imported rather than redefined, from the published definition bundle of the companion
mission, where it is the subgroup generated by the piecewise-linear maps described above;
membership in that subgroup is identified with the piecewise-linear description by a theorem
already machine-checked there. Exponent data is carried by finite lists, and the uniqueness in
the goal is uniqueness of that list data.
The goal is vacuous in neither direction: its hypothesis is met by $A$ and $B$ themselves, and a
separate milestone asserts that every choice of exponent data meeting the two conditions names an
element other than the identity.
The tree combinatorics — leaf counts, right sides, the subdivision map, the exponents,
carets — is published here as a separate definition node that mentions $F$ nowhere and needs
nothing but Mathlib, so it is reusable as it stands; the diagram vocabulary is built on it. Any
milestone is open to contribution, as are routes other than the paper's.
## Selected references
- J. W. Cannon, W. J. Floyd, W. R. Parry, *Introductory notes on Richard Thompson's groups*,
L'Enseignement Mathématique (2) **42** (1996), 215–256.
[doi:10.5169/seals-87877](https://doi.org/10.5169/seals-87877) — §2, pages 218–224, is the
source for this mission; §1, page 217, defines $A$, $B$ and the $X_n$.
Within that paper tree diagrams are credited to Brown and the word-length algorithm to Fordham,
cited there as [Bro1] and [Fo].
Magic Squares I: MacMahon's Enumeration of Order-Three Magic SquaresResearch Paper
## Motivation
Counting **magic squares** — arrays of nonnegative integers whose rows, columns
and two main diagonals all share a common line sum — is one of the oldest
problems in enumerative combinatorics, and the testing ground on which the
general theory was built. MacMahon computed the order-three count in 1915 by
hand; sixty years later Stanley, and then Beck, Cohen, Cuomo and Gribelyuk
([*Amer. Math. Monthly* **110** (2003), 707--717](https://arxiv.org/abs/math/0201013)),
showed that for *general* order $n$ the counting functions are
**quasi-polynomials** in the line sum, by identifying them with Ehrhart
quasi-polynomials of rational polytopes. The order-three case is the oldest
nontrivial instance of that theory and the one where every step can still be
checked by hand.
The subject therefore has a curious status: the enumerative answer for $n=3$ has
been known for over a century, and the *structural* facts behind it (a
$3\times3$ magic square is determined by two corner entries; opposite cells sum
to twice the centre) are folklore — but none of it has a machine-checked proof.
This mission formalizes the classical derivation end to end.
## Setting
Fix an order $n$ and a type $\alpha$ of entries. A **square** of order $n$ is an
$n\times n$ array $M$ with entries in $\alpha$; its **row sums**, **column
sums**, and the two **diagonal sums** (main and anti-diagonal) are the sums of
the entries along those lines.
* $M$ is **semi-magic** with line sum $s$ if every row and every column sums to
$s$.
* $M$ is **magic** with line sum $s$ if in addition both main diagonals sum to
$s$.
* $M$ is **panmagic** (pandiagonal) if every *broken* diagonal, in both
directions, also sums to $s$.
No distinctness of entries is required. Let $H_n(t)$ denote the number of
semi-magic and $M_n(t)$ the number of magic squares of order $n$ with
nonnegative integer entries and line sum $t$. Every entry of such a square is at
most $t$, so these are finite counts.
For $n=3$ the whole family is parametrized. If $M$ has line sum $3e$ then the
centre cell equals $e$, and writing $a=M_{00}$ and $c=M_{02}$ the eight line
identities force
$$
M=\begin{pmatrix}
a & 3e-a-c & c\\
e+c-a & e & e+a-c\\
2e-c & a+c-e & 2e-a
\end{pmatrix}.
$$
All nine entries are nonnegative exactly when
$$
e\le a+c\le 3e,\qquad a\le e+c,\qquad c\le e+a,
$$
and substituting $p=a-e$, $q=c-e$ turns these into $|p|+|q|\le e$: the
$\ell_1$ ball of radius $e$ in $\mathbb{Z}^2$.
## Formalization targets
### Goal — MacMahon's count
$$M_{3}(3e)\;=\;2e^{2}+2e+1 ,$$
together with the companion vanishing $M_3(t)=0$ when $3\nmid t$. This is the
count of $3\times3$ **magic** squares of line sum $3e$ with nonnegative integer
entries (entries need not be distinct). It is the goal because it is the
weakest stable statement: it asserts only the shape of the answer, not the
intermediate parametrization, and it survives verbatim as the $n=3$ case of the
general quasi-polynomial theorem.
### Stronger — the parametrization itself
That the map $M\mapsto(M_{00},M_{02})$ is a **bijection** from the $3\times3$
magic squares of line sum $3e$ onto the admissible parameter pairs, and that the
latter are counted by the $\ell_1$-ball cardinality. This is the route the
mission actually takes; the count is its corollary.
### Further — semi-magic counts
$H_3(t)$, the analogous count for **semi-magic** squares, is a genuinely
different and harder quasi-polynomial. It is listed as a stretch target, not a
milestone.
## Significance
*The result itself.* MacMahon's formula is the base case of the Ehrhart-theory
reading of magic-square enumeration; Beck--Cohen--Cuomo--Gribelyuk's
quasi-polynomial theorem for general $n$ degenerates to it at $n=3$, so it is
the sanity check any generalization must pass. The parametrization behind it is
what makes the "how many" question finite-dimensional at all: it reduces a
search over $t^9$ arrays to a count of lattice points in a two-dimensional ball.
Downstream, the same parametrization governs the classification of *normal*
$3\times3$ magic squares (the Lo Shu square and its symmetries) and the
associativity identity $M_{ij}+M_{2-i,2-j}=2M_{11}$.
*Formalizing it.* The mathematics is classical and **proved**; nothing here is
open. What is missing is the **formalized** artifact. The order-three structural
lemmas — the centre identity, the opposite-cell identity, and the two directions
of the parametrization — are already machine-checked on this platform. The
remaining work is the *counting* step: exhibiting a concrete bijection between
two finsets whose elements live in different types (arrays over `Fin (3e+1)`
versus pairs of naturals) and evaluating a finite sum. That is where the
formalization, not the mathematics, is hard.
## Difficulty
The obvious attack — "each magic square is determined by $(a,c)$, so just count
the pairs" — fails at exactly one point, and it is not a mathematical point. The
counting function $M_3$ is defined as the cardinality of a finset of arrays with
entries in `Fin (3e+1)` (a *finite* type, so that `Finset.univ` exists), whereas
the parametrization lives over $\mathbb{N}$. Proving the counts agree therefore
requires a honest `Finset.card_bij` in **both** directions:
* forward, extract $(M_{00},M_{02})$ from an array and show the pair is
admissible;
* backward, build `mkMagic3` from an admissible pair, coerce every entry into
`Fin (3e+1)` using the bound $M_{ij}\le 2e\le 3e$, and show the round trip is
the identity.
Neither direction is deep, but the coercions are unforgiving: a truncated
subtraction in `mkMagic3` is only correct because admissibility forbids the
truncation, and that side condition must be discharged explicitly rather than
assumed. The second difficulty is the cardinality of the $\ell_1$ ball: the
identification $|p+q|\le e\ \wedge\ |p-q|\le e\ \Longleftrightarrow\
|p|+|q|\le e$ needs the elementary identity
$\max(|p+q|,|p-q|)=|p|+|q|$, after which the count is
$1+4\sum_{k=1}^e k = 2e^2+2e+1$.
## Formalization scope
* Entries are indexed by `Fin n`; the anti-diagonal uses `Fin.rev`, and broken
diagonals use addition modulo $n$. Counting functions are cardinalities of
finsets of arrays over `Fin (t+1)` — lossless, since every entry is at most
$t$ — and return natural numbers.
* `mkMagic3` is defined over $\mathbb{N}$ with **truncated** subtraction. Every
row/column/diagonal identity therefore carries the admissibility inequalities
as explicit hypotheses; no identity is asserted unconditionally.
* Trivializing formalizations are ruled out: the goal is not a statement about a
hardcoded small $e$, nor about a finset declared to have the right
cardinality. The count must be *derived*.
* Reusable beyond this mission: the core vocabulary (`Square`, `IsSemiMagic`,
`IsMagic`, `IsPanMagic`, `IsAssociative`, `IsNormal`, `magicConstant`, and the
four counting functions $H_n,M_n,P_n,S_n$), the symmetry/affine toolbox, and
the order-three structural lemmas. Contributions are welcome on the
semi-magic count $H_3$, on panmagic and associative refinements, and on the
extension to general $n$.
## Selected references
- P. A. MacMahon, *Combinatory Analysis*, Vol. II, Cambridge University Press, 1916 (the $M_3$ formula dates to his 1915 work).
- M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, *The number of "magic" squares, cubes and hypercubes*, Amer. Math. Monthly **110** (2003), 707--717. <https://arxiv.org/abs/math/0201013>
- M. Beck and T. Zaslavsky, *Six little squares and how their numbers grow*, J. Combin. Theory Ser. A **113** (2006). <https://arxiv.org/abs/math/0502370>
- G. Xin, *Constructing all magic squares of order three*, Discrete Math. **308** (2008). <https://arxiv.org/abs/math/0610771>
## Motivation
An **online algorithm** must commit to decisions before it knows the rest of its input, and it is judged by **competitive analysis**: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.
This mission formalizes the chapter where the method is introduced on its smallest example, the **ski-rental problem**. A customer needs skis for an unknown number of days: renting costs $1$ per day and buying costs $B$ once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic $2$-competitive algorithm, and a randomized algorithm whose competitive ratio tends to $e/(e-1)$, due to [Karlin, Manasse, McGeoch and Owicki (1994)](https://doi.org/10.1007/BF01294260). The primal-dual derivation of both is the content of Chapter 3.
## Setting
An instance is a pair $(B, k)$: the **purchase price** $B$, a positive integer, and the number $k \ge 0$ of **ski days**, which the online algorithm does not know. An offline solution either buys at once, paying $B$, or rents on every day, paying $k$; so the **offline optimum** is
$$\mathrm{OPT}(B,k) \;=\; \min(B, k).$$
Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The **primal** is a covering program with one buy variable $x$ and one rent variable $z_j$ per day $j$:
$$\text{minimize } \; B x + \sum_{j=1}^{k} z_j \quad \text{subject to} \quad x + z_j \ge 1 \ \text{ for each day } j.$$
Its **dual** is a packing program with one variable $y_j$ per day:
$$\text{maximize } \; \sum_{j=1}^{k} y_j \quad \text{subject to} \quad \sum_{j=1}^{k} y_j \le B, \qquad 0 \le y_j \le 1 .$$
The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.
The **fractional primal-dual algorithm** maintains $x$, initially $0$. On each new day, while $x < 1$ it sets $z_j \leftarrow 1 - x$, then raises
$$x \;\leftarrow\; x\left(1 + \tfrac{1}{B}\right) + \tfrac{1}{cB},$$
and sets $y_j \leftarrow 1$; once $x$ has reached $1$ it does nothing further. The free parameter $c$ is then pinned to the value that makes $x$ reach exactly $1$ after $B$ days,
$$c \;=\; \left(1 + \tfrac{1}{B}\right)^{B} - 1 .$$
## Formalization targets
### Goal — the fractional algorithm's competitive ratio at finite $B$
$$B\,x_k + \sum_{j=0}^{k-1} z_j \;\le\; \left(1 + \frac{1}{\left(1 + \frac{1}{B}\right)^{B} - 1}\right) \cdot \min(B, k) \qquad \text{for every } B \ge 1, \ k \ge 0 .$$
The coefficient is the exact finite-$B$ ratio $1 + 1/c$, left in closed form rather than replaced by a constant. This is deliberate: $\left(1+\frac1B\right)^B$ increases to $e$, so $c < e - 1$ and therefore $1 + 1/c > e/(e-1)$ for every finite $B$. A goal asserting $e/(e-1)$-competitiveness at finite $B$ would be **false**, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.
### Asymptotic companion — where $e/(e-1)$ actually lives
$$\lim_{B \to \infty} \left(1 + \frac{1}{\left(1 + \frac{1}{B}\right)^{B} - 1}\right) \;=\; \frac{e}{e-1} \;\approx\; 1.5819767 .$$
The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.
### Parallel target — the deterministic algorithm
$$\mathrm{detCost}(B,k) \;\le\; 2 \cdot \min(B,k), \qquad \mathrm{detCost}(B,k) = \begin{cases} k & k < B \\ 2B & k \ge B\end{cases}$$
Chapter 3's other result, independent of the fractional development.
## Significance
The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the *derivation*: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.
On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision `0df444a`, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.
## Difficulty
The offline problem is trivial, and a newcomer's first move — prove $\min(B,k)$ is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:
**The optimum is never observed.** The algorithm's cost must be compared against $\min(B,k)$ without $k$ being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.
**The growth law is piecewise.** The update fires only while $x < 1$. Summing the per-day increments therefore does not telescope uniformly: days before $x$ reaches $1$ contribute $1 + 1/c$ each and later days contribute nothing, and the index at which the switch happens is exactly $B$ — which is a theorem about the recurrence, not an assumption.
**The constant is forced, not chosen.** $c = (1+1/B)^B - 1$ is not a free tuning parameter; it is the unique value for which the geometric sequence $x_j = \bigl((1+1/B)^j - 1\bigr)/c$ hits $1$ at $j = B$, which is in turn what makes the dual solution feasible ($\sum_j y_j \le B$). Dual feasibility and the choice of $c$ are the same fact.
## Formalization scope
**Conventions this development commits to.** The purchase price is a natural number $B$ with $0 < B$, because Chapter 3 uses $B$ simultaneously as a price, as a day index ("buy skis on the $B$th day"), and as the exponent in $(1+1/B)^B$; costs are real numbers, with $B$ and $k$ coerced. Days are indexed from $0$, so day $j+1$ of the prose is index $j$, and `Fin k` indexes the $k$ days. Real division is total, so $1/0 = 0$; the hypothesis $0 < B$ is what keeps every reciprocal in the development genuine, and without it $c$ would evaluate to $0$ and the recurrence would collapse to the constant zero sequence. The algorithm's `x < 1` guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day $B$.
**A documented discrepancy in the source.** The prose on p. 17 relaxes the integer program by letting $x$ and each $z_j$ range over $[0,1]$; Figure 3.1 on p. 18 prints only $x \ge 0$, $z_j \ge 0$. This mission takes the prose version, $0 \le x \le 1$ and $0 \le z_j \le 1$, as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value $\min(B,k)$, so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.
**Ruling out a trivializing formalization.** The offline optimum is *defined* independently, as $\min(B,k)$, and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to $(1+1/c)$ times the number of days on which $x < 1$ — so it cannot be weakened into vacuity without becoming false.
**Infrastructure, and what is reusable.** The development needs only `Mathlib` big operators over `Fin k`, basic real analysis for the limit, and `IsLeast`. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.
**Out of scope here.** The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold $\alpha \in [0,1]$ uniformly and buying on the day whose increment of $x$ contains $\alpha$. That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, *Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental*. Contributions here should not anticipate it.
## Selected references
- Niv Buchbinder, *Designing Competitive Online Algorithms via a Primal-Dual Approach*, PhD thesis, Tel Aviv University, 2008. Chapter 3, pp. 17–19. <https://www.tau.ac.il/~nivb/download/phd-thsis.pdf>
- Niv Buchbinder and Joseph (Seffi) Naor, *The Design of Competitive Online Algorithms via a Primal-Dual Approach*, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. <https://doi.org/10.1561/0400000024>
- Anna R. Karlin, Mark S. Manasse, Lyle A. McGeoch and Susan Owicki, *Competitive randomized algorithms for nonuniform problems*, Algorithmica 11(6), 1994, 542–571. <https://doi.org/10.1007/BF01294260>
- Allan Borodin and Ran El-Yaniv, *Online Computation and Competitive Analysis*, Cambridge University Press, 1998.
Discriminative Kalman Filter asymptoticsResearch Paper
## Motivation
**Bayesian filtering** estimates an unobserved state from measurements arriving over time. A filter combines what the state dynamics predict with what the newest observation says. In neural decoding, for example, the state may describe an intended movement while the observation contains activity from many recorded neurons. The observation can have many more coordinates than the state and need not follow a linear Gaussian observation model.
The **Discriminative Kalman Filter (DKF)** uses a Gaussian approximation to the state conditional on the newest observation. It combines that approximation with a Gaussian state transition and a correction for the stationary state distribution. The resulting recursion retains a mean vector and covariance matrix. Burkhart et al. developed this construction and proved an asymptotic justification in [Theorem 2 of Appendix B](https://doi.org/10.1162/neco_a_01275).
The historical starting point is the linear Gaussian filter of [Kalman (1960)](https://doi.org/10.1115/1.3662552). The 2020 DKF paper changes how observation information enters the update and establishes a corresponding approximation theorem. The present mission concerns formal verification of that published theorem.
## Setting
The state space is $\mathbb R^d$ for a positive finite dimension $d$. Write $\eta_d(z;m,C)$ for the ordinary multivariate Gaussian density with mean $m$ and symmetric positive-definite covariance $C$. Densities and their $L^1$ distances are with respect to Lebesgue measure.
The state model has a matrix $A$ and positive-definite covariance matrices $\Gamma,S$ satisfying
$$S=ASA^\top+\Gamma.$$
Its stationary density and transition density are
$$p(z)=\eta_d(z;0,S),\qquad \tau(y,z)=\eta_d(z;Ay,\Gamma).$$
For an integrable density $s$, prediction gives
$$ (\tau s)(z)=\int\tau(y,z)s(y)\,dy.$$
The discriminative update combines a previous filtering density $s$ with a density $u$ for the state given the current observation:
$$\frac{u\,\tau s/p}{\|u\,\tau s/p\|_1}.$$
This expression is a probability density when its nonnegative weight has a finite, strictly positive integral. Dividing by $p$ is part of the standard DKF under consideration.
For Gaussian inputs with parameters $(a,V)$ and $(b,U)$, define
$$G=AVA^\top+\Gamma,\qquad T=(U^{-1}+G^{-1}-S^{-1})^{-1},$$
$$c=T(U^{-1}b+G^{-1}Aa).$$
The DKF step returns mean $c$ and covariance $T$ when the precision is invertible and the covariance is positive definite. The recursive filter starts from mean zero and covariance $S$, using the current observation's functions $f$ and $Q$ as the Gaussian input mean and covariance. These are the updates in equation (2.7) of the [paper](https://doi.org/10.1162/neco_a_01275).
## Formalization targets
Fix sequences of probability densities $s_n,u_n$, indexed by positive integers, whose exact normalized updates
$$p_n=\frac{u_n\tau s_n/p}{\|u_n\tau s_n/p\|_1}$$
are well defined for every index. Fix Gaussian density sequences $s'_n,u'_n$, a point $b$, and a probability measure $P$. The five assumptions are
$$\begin{aligned}
\mathrm{A1}:&\quad s_n\Rightarrow P,\\
\mathrm{A2}:&\quad \|s_n-s'_n\|_1\longrightarrow0,\\
\mathrm{A3}:&\quad u_n\Rightarrow\delta_b,\\
\mathrm{A4}:&\quad \|u_n-u'_n\|_1\longrightarrow0,\\
\mathrm{A5}:&\quad p_n\Rightarrow\delta_b.
\end{aligned}$$
Here $\Rightarrow$ denotes weak convergence, characterized by convergence of expectations of every bounded continuous real function; $\delta_b$ is the unit point mass at $b$. The measure $P$ need not have a density and may be degenerate.
The main goal is the complete conjunction of Theorem 2's conclusions, with separate milestones for each:
- **C1:** $s'_n\Rightarrow P$.
- **C2:** $u'_n\Rightarrow\delta_b$.
- **C3:** the specific update
$$p'_n=\frac{u'_n\tau s'_n/p}{\|u'_n\tau s'_n/p\|_1}$$
is a well-defined Gaussian density for all sufficiently large $n$.
- **C4:** $p'_n\Rightarrow\delta_b$.
- **C5:** $\|p_n-p'_n\|_1\longrightarrow0$.
A sixth milestone is **Lemma 1 (DKF equation)**: the normalized Gaussian-input update has the explicit mean and covariance above whenever valid, and the two input weak limits imply its eventual validity and convergence to $\delta_b$. It includes both the exact equation and the asymptotic assertion from the source.
## Significance
In addition to neurodecoding with intracortical brain-computer interfaces, the DKF has also found applications in optimization and sequential data augmentation (see references). The original study was successfully reproduced by Casco-Rodriguez, et al. in ReScience C.
## Difficulty
The inverse stationary density can grow in the tails, so small $L^1$ errors in the input densities do not immediately control the error after division and renormalization. Normalizing constants must remain finite and nonzero. The candidate Gaussian covariance must also become positive definite as a conclusion of the assumptions, rather than through an extra validity assumption imposed at every index.
There is a second distinction between convergence to a point mass and approximation in $L^1$. Two sequences may concentrate at the same point while retaining different shapes at shrinking scales. The C5 target therefore requires the full approximation argument, beyond the weak-convergence conclusions.
## Formalization scope
Lean represents states as `Fin d → ℝ` and covariance matrices as real square matrices. The Gaussian density is the standard determinant-and-quadratic-form formula. The definition of Gaussian PDF includes positive-definite covariance and equality of densities almost everywhere. Thus null-set changes do not constrain the theorem artificially.
Probability density validity explicitly includes nonnegativity almost everywhere, integrability and total integral one. The $L^1$ quantity is an extended nonnegative integral. The update's validity explicitly requires measurable weight and a finite, strictly positive normalizer. Total expressions outside that domain supply no assumed probability interpretation; C3 establishes validity on a tail.
All density sequences use positive integer indices. The limit measure is a Mathlib probability measure. Weak convergence is tested against Mathlib bounded continuous functions using the actual measures generated by the densities. The stationary model, standard recursive DKF, exact update and approximate update are defined independently of the theorem conclusions.
The mission addresses deterministic Theorem 2 of Appendix B. The random-sequence extension in Remark 4, conditions implying a Bernstein–von Mises theorem, and induction over filtering time are separate developments. The proof plan follows the appendix through C1–C2, Lemma 1, C3–C4, and the five-term comparison for C5.
## Selected references
- M. C. Burkhart, D. M. Brandman, B. Franco, L. R. Hochberg and M. T. Harrison, *The Discriminative Kalman Filter for Bayesian Filtering with Nonlinear and Nongaussian Observation Models*, Neural Computation 32(5), 969–1017, 2020. [DOI: 10.1162/neco_a_01275](https://doi.org/10.1162/neco_a_01275).
- R. E. Kalman, *A New Approach to Linear Filtering and Prediction Problems*, Journal of Basic Engineering 82(1), 35–45, 1960. [DOI: 10.1115/1.3662552](https://doi.org/10.1115/1.3662552).
- M. C. Burkhart, *A Discriminative Approach to Bayesian Filtering with Applications to Human Neural Decoding*, Ph.D. dissertation, Brown University, 2019. [DOI: 10.26300/nhfp-xv22](https://doi.org/10.26300/nhfp-xv22).
- D. M. Brandman, M. C. Burkhart, J. Kelemen, B. Franco, M. T. Harrison and L. R. Hochberg, *Robust Closed-Loop Control of a Cursor in a Person with Tetraplegia using Gaussian Process Regression*, Neural Computation 30(11), 2986–3008, 2018. [DOI: 10.1162/neco_a_01129](https://doi.org/10.1162/neco_a_01129).
- D. M. Brandman, T. Hosman, J. Saab, M. C. Burkhart, B. E. Shanahan, J. G. Ciancibello et al., *Rapid calibration of an intracortical brain–computer interface for people with tetraplegia*, Journal of Neural Engineering 15(2), 026007, 2018. [DOI: 10.1088/1741-2552/aa9ee7](https://doi.org/10.1088/1741-2552/aa9ee7).
- J. Casco-Rodriguez, C. Kemere and R. G. Baraniuk, *[Re] The Discriminative Kalman Filter for Bayesian Filtering with Nonlinear and Non-Gaussian Observation Models*, ReScience C 10(1), article 3, 2025. [DOI: 10.5281/zenodo.15172014](https://doi.org/10.5281/zenodo.15172014), [published PDF](https://zenodo.org/record/15172014/files/article.pdf).
- M. C. Burkhart, *Discriminative Bayesian filtering lends momentum to the stochastic Newton method for minimizing log-convex functions*, Optimization Letters 17, 657–673, 2023. [DOI: 10.1007/s11590-022-01895-5](https://doi.org/10.1007/s11590-022-01895-5).
Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem
## 1. Motivation
Wikipedia's pages on open problems are, for many mathematicians, the first contact with a
conjecture: a one-paragraph statement, a short history, a list of partial results. The
[Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) library (Google
DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the
conjectures can be attacked — and, just as importantly, *stated unambiguously* — by machine.
This mission ports a coherent slice of that material to Prove2Me. It is deliberately a
**portfolio mission**: the goal theorem is the Bateman–Horn conjecture, the strongest single
statement in the collection, and the milestone list gathers the other conjectures and the
landmark theorems that surround them. Some milestones are genuine steps toward the goal (the
Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems
from other fields, grouped here because they share a source, a level of difficulty, and a need
for faithful formal statements. **A reader should not assume that proving a milestone advances
the goal theorem.** The mission's value is that every statement in it has been written against
the same Mathlib revision, checked to compile, and documented well enough to be attacked.
A rough timeline of the collection's landmarks:
- 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
- 1962 — Radó: the busy beaver function outgrows every computable function.
- 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
- 1978 — Apéry: $\zeta(3)$ is irrational.
- 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant
subspace.
- 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
- 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
- 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
- 2021 — Gardam: Kaplansky's *unit* conjecture is false (its zero-divisor and idempotent
companions remain open).
- 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
- 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.
## 2. Setting
The goal theorem concerns prime values of polynomials. Fix a finite set
$S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the
**Bunyakovsky condition** if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is
irreducible over $\mathbb{Z}$; say that $S$ satisfies the **Schinzel condition** if for every
prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides
the product at every argument.
For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some
$f_i$ vanishes, let $D=\prod_i \deg f_i$, and let
$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$
The **Bateman–Horn constant** is the (conditionally convergent) Euler product
$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$
The other groups use their own vocabulary, each fixed in a definition item of this mission:
Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property
$\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial
self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of
a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its
maximum-shifts function $\mathrm{BB}$.
## 3. Target
The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses,
$C$ exists and is positive and
$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$
Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's
conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The
remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine
equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality
(New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants
(Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$,
Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample),
group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry
(the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta
values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the
$1/3$–$2/3$ conjecture), and computability (Radó's theorem).
## 4. Significance
*The results themselves.* Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it
contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky
as special cases, and it is the standard heuristic behind prime-counting predictions. The other
targets are each the headline question of their area: whether every bounded Hilbert-space
operator has an invariant subspace; whether group algebras of torsion-free groups are domains;
whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir,
Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library
contributions in their own right.
*Formalizing them.* None of the open statements is expected to fall here; the concrete deliverable
is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones,
most of which are not in Mathlib today. Several are realistically in reach: the finite-field
Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$
cannot both be algebraic, and Radó's diagonal argument.
## 5. Difficulty
For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound
$\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes,
but the parity problem blocks every known sieve from producing a single prime value of an
irreducible quadratic. The conditional convergence of the Euler product is a second, smaller
trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered
infinite product changes the statement.
Each other group has its own obstruction, and they do not transfer: the parity problem says
nothing about Kakeya, where the difficulty is that dimension is not stable under the natural
compactness arguments, nor about the invariant subspace problem, where the known counterexamples
on $\ell^1$ show that no soft argument can work.
## 6. Formalization scope
Conventions this mission commits to, all fixed in the definition items:
- Polynomials are elements of `ℤ[X]`; primality of a polynomial value is primality of its
absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
- The Bateman–Horn constant is the limit of the *ordered* partial products over $p<N$, not an
unordered infinite product.
- Kakeya sets carry no compactness or measurability hypothesis, matching the source; the
conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
- Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
- Torsion-freeness of a group is spelled out as "every element of finite order is the identity",
which is the hypothesis the source intends (it is weaker than Mathlib's `IsMulTorsionFree`).
- Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities
are quotients of set cardinalities in $\mathbb{Q}$.
- The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean
tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition
included, and $\mathrm{BB}(0)=0$.
- Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me
statements must be definite, so each such question is recorded in its **affirmative** form
(e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one
question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth
theorem rather than guessed at.
- Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya
sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).
Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful
statements from the same source library, which contains far more than fits in one mission.
## 7. Selected references
- P. T. Bateman and R. A. Horn, *A heuristic asymptotic formula concerning the distribution of
prime numbers*, Math. Comp. 16 (1962), 363–367.
[DOI](https://doi.org/10.1090/S0025-5718-1962-0148632-7)
- T. Radó, *On non-computable functions*, Bell System Tech. J. 41 (1962), 877–884.
[DOI](https://doi.org/10.1002/j.1538-7305.1962.tb00480.x)
- R. O. Davies, *Some remarks on the Kakeya problem*, Math. Proc. Cambridge Philos. Soc. 69
(1971), 417–421. [DOI](https://doi.org/10.1017/S0305004100046867)
- C. J. Read, *A solution to the invariant subspace problem on the space $\ell_1$*, Bull. London
Math. Soc. 17 (1985), 305–317. [DOI](https://doi.org/10.1112/blms/17.4.305)
- K. Falconer, *On the Hausdorff dimensions of distance sets*, Mathematika 32 (1985), 206–212.
[DOI](https://doi.org/10.1112/S0025579300010998)
- W. Zudilin, *One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational*, Russian
Math. Surveys 56 (2001), 774–776. [DOI](https://doi.org/10.1070/RM2001v056n04ABEH000427)
- P. Mihăilescu, *Primary cyclotomic units and a proof of Catalan's conjecture*, J. reine angew.
Math. 572 (2004), 167–195. [DOI](https://doi.org/10.1515/crll.2004.048)
- Z. Dvir, *On the size of Kakeya sets in finite fields*, J. Amer. Math. Soc. 22 (2009),
1093–1097. [DOI](https://doi.org/10.1090/S0894-0347-08-00607-3)
- B. Bukh and T.-W. Chao, *Sharp density bounds on the finite field Kakeya problem*, Discrete
Analysis 26 (2021). [DOI](https://doi.org/10.19086/da.30071)
- G. Gardam, *A counterexample to the unit conjecture for group rings*, Ann. of Math. 194 (2021),
967–979. [DOI](https://doi.org/10.4007/annals.2021.194.3.9)
- K. Saito, *Mills' constant is irrational*, Mathematika 71 (2025), e70027.
[arXiv:2404.19461](https://arxiv.org/abs/2404.19461)
- H. Wang and J. Zahl, *Volume estimates for unions of convex sets, and the Kakeya set conjecture
in three dimensions*, [arXiv:2502.17655](https://arxiv.org/abs/2502.17655)
- Google DeepMind, *Formal Conjectures*, Apache-2.0,
[github.com/google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures)
---
*Provenance note.* The Lean statements in this mission are adaptations of the Formal Conjectures
library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition
items, and checked to compile against the platform's Mathlib revision. Each draft item carries a
read-back; **those read-backs are non-blind** — they were written by the same agent that drafted
the statements, and each says so in its first line. They are documentation, not independent
testimony.
Cannon–Floyd–Parry: Thompson's group F and the simplicity of its commutator subgroupTextbook
## Motivation
This mission formalizes §4 of Cannon, Floyd and Parry's *Introductory notes on Richard
Thompson's groups*, together with the definition of **Thompson's group $F$** from their §1.
The goal is their Theorem 4.5: the commutator subgroup $[F,F]$ is simple.
In the 1960s Richard Thompson defined three groups, now written $F$, $T$ and $V$, whose
properties have kept them in use ever since as a source of examples at the edge of what
groups can do. $F$ is the smallest of the three and the least understood. It is finitely
presented (§3 of the source) and torsion-free, it has no free subgroup of rank two, and
whether it is **amenable** — whether it carries a finitely additive left-invariant probability
measure defined on all its subsets — is open. Cannon, Floyd and Parry record (§4, p. 227) that
Geoghegan raised the question and conjectured in 1979 both that $F$ contains no non-Abelian
free subgroup and that $F$ is not amenable.
That question is what makes $F$ worth pinning down precisely. Write $AG$ for the class of
amenable discrete groups, $EG$ for the elementary amenable ones, and $NF$ for the groups with
no free subgroup of rank two. That $AG \subset NF$ was noted by
[Day](https://doi.org/10.1215/ijm/1255380675) and follows from
[von Neumann](https://doi.org/10.4064/fm-13-1-73-116); whether it is strict is the **von
Neumann–Day problem**. It is: Olshanskii proved $AG \neq NF$ in a 1984 ICM address and
[Gromov](https://doi.org/10.1007/978-1-4613-9586-7_3) gave an independent proof — but by
examples that are not finitely presented. Brin and Squier proved in 1985 that $F \in NF$, and
$F$ is known not to be elementary amenable (Theorem 4.10 of the source, out of scope here). So
$F$ is a finitely presented group in $AG \setminus EG$ if it is amenable and in
$NF \setminus AG$ if it is not — a question with no other finitely presented candidate.
## Setting
Call a real number **dyadic** if it has the form $m/2^{k}$ with $m \in \mathbb{Z}$ and
$k \in \mathbb{N}$.
**Thompson's group $F$**, as §1 of the source defines it, is the set of piecewise linear
homeomorphisms of the closed unit interval $[0,1]$ onto itself that are differentiable except
at finitely many dyadic rationals, and whose derivatives, where they exist, are powers of $2$.
Since those derivatives are positive, every element preserves orientation, so the elements of
$F$ are increasing. Composition of two such maps is again one, and so is the inverse of one,
so $F$ is a group.
The formalization calls such a map **piecewise linear over the dyadics**, and defines $F$ as
the subgroup *generated by* those maps — so that closure under composition and inverses is a
theorem rather than part of the construction, as the source has it. What the model fixes rather
than derives is under **Formalization scope** below.
Two particular elements generate it. Write
$$A(x) = \begin{cases} x/2 & 0 \le x \le \tfrac12\\ x - \tfrac14 & \tfrac12 \le x \le \tfrac34\\ 2x-1 & \tfrac34 \le x \le 1\end{cases}
\qquad
B(x) = \begin{cases} x & 0 \le x \le \tfrac12 \\ x/2 + \tfrac14 & \tfrac12 \le x \le \tfrac34 \\ x - \tfrac18 & \tfrac34 \le x \le \tfrac78 \\ 2x-1 & \tfrac78 \le x \le 1.\end{cases}$$
An element of $F$ is **trivial near $0$** if it fixes every point of some interval
$[0,\varepsilon)$, and **trivial near $1$** if it fixes every point of some
$(1-\varepsilon, 1]$. The **support** of $f$ is the set of points of $[0,1]$ that $f$ moves.
The commutator convention throughout is $[x,y] = xyx^{-1}y^{-1}$, and $[F,F]$ denotes the
commutator subgroup.
## Formalization targets
### Goal
$$[F,F] \ \text{is a simple group.}$$
This is the capstone of §4: it says the commutator subgroup has no normal subgroup other than
itself and the trivial one. It is the goal because the rest of the section feeds it — both
halves of Theorem 4.1, Theorem 4.3, and both supporting lemmas below are consumed by its
proof.
### Theorem 4.1, which has two parts
$$[F,F] \;=\; \{\, f \in F : f \text{ is trivial near } 0 \text{ and near } 1 \,\}$$
$$F/[F,F] \;\cong\; \mathbb{Z} \oplus \mathbb{Z}$$
### Theorem 4.3
$$N \trianglelefteq F,\ N \neq 1 \;\Longrightarrow\; F/N \text{ is Abelian}$$
So $F$ has no interesting proper quotients at all. With the first part of Theorem 4.1 this
forces every nontrivial normal subgroup of $F$ to contain $[F,F]$.
### Supporting results
That the piecewise-linear maps are already closed under composition and inverses, so that $F$
consists of exactly those maps; a transitivity lemma on dyadic partitions of $[0,1]$; the fact
that the subgroup of elements supported in a dyadic interval $[a,b]$ of dyadic length is
isomorphic to $F$ itself; triviality of the center; that $F$ contains no non-Abelian free group;
and that $F$ admits a total order invariant under multiplication on both sides.
## Significance
**What the results give.** Theorem 4.1 identifies $[F,F]$ concretely — a subgroup defined by a
global algebraic condition turns out to be cut out by local behavior at the two endpoints —
and computes the abelianization, making the pair of endpoint slopes a complete invariant of $F$
modulo commutators. Theorem 4.3 and the simplicity of $[F,F]$ together determine the whole
normal subgroup lattice: every normal subgroup of $F$ is trivial or contains $[F,F]$. That
lattice is the input to the elementary-amenability argument.
**What formalizing adds.** All of these are proved in the source; none is in Mathlib, which
has no piecewise-linear homeomorphism API and no Thompson group. Four of the milestones are
proved as part of this proposal: that the piecewise-linear maps form a subgroup, that elements
of $F$ permute the dyadic rationals, that $F$ embeds in the group Brin and Squier work with, and
the absence of a free subgroup of rank two, which follows from the already-formalized
Brin–Squier theorem via that embedding. The rest are open. The piecewise-linear machinery built along the way — local affineness,
dyadic-breakpoint bookkeeping, extension by the identity — is reusable for $T$, for $V$, and
for the wider family of piecewise-linear homeomorphism groups.
## Difficulty
The obvious approach to the goal is to argue that a normal subgroup of $[F,F]$ containing a
nontrivial element must be everything, by conjugating that element around. It fails on its own:
an element of $[F,F]$ is pinned down only by being trivial near the two endpoints, and one still
has to manufacture — inside $[F,F]$, not merely inside $F$ — an element carrying a prescribed
pair of neighborhoods into those. That construction is what the dyadic-partition transitivity
lemma supplies, and it is where the combinatorics of dyadic subdivision enters.
The second difficulty was that the source proves §4 using the tree-diagram normal form of §2.
That section is now formalized in its own mission, *Cannon–Floyd–Parry §2: tree diagrams and the
normal form* (mission `ffd1e4ea-9f9a-4cb6-8419-78e70f2545e8`), all of whose milestones are proved.
Corollary 2.6 — milestone 5 here, the same theorem object — is closed from there, and Theorem
2.5 (`represents_word_exponents`) and the normal form (`existsUnique_normalForm`) are available to
a solver attacking Theorem 4.3, so the source's argument can now be followed. A solution file
imports only definitions, so whatever it uses from §2 must be reproved inline; the §2 solutions
are public and written to be reused that way. The piecewise-linear route — dyadic-partition
transitivity, Lemma 4.4 and Theorem 4.1 — remains an alternative, and is what Theorem 4.5's own
argument uses.
## Formalization scope
The unit interval is $[0,1] \subseteq \mathbb{R}$ as a subtype, and an element of $F$ is an
order isomorphism of it, so orientation preservation is built into the representation rather
than derived — faithful to the source's set, but assuming one sentence CFP prove. Piecewise
linearity is stated as: there is a finite set $B$ of dyadic reals such that the map is affine,
with slope a power of two, on every closed interval whose interior misses $B$. Intercepts are
**not** required to be dyadic — that is derived by induction along the breakpoints, not part of
the definition.
The definition is not vacuous: $A$ and $B$ of Example 1.1 are constructed explicitly, and that
$F$ is not the trivial group is one of the milestones below — so no statement here is satisfied
by the trivial group. In particular the goal, which asserts simplicity and therefore
nontriviality, is not trivially false.
A companion definition places the same data on the real line, each element extended by the
identity outside $[0,1]$; that line realisation is what the bridge statement connects to Brin
and Squier's group. Corollaries 4.6, 4.7 and 4.10 of the source are out of scope: they need free
products of monoids, growth of finitely generated groups, and the transfinite class of
elementary amenable groups respectively, none of which Mathlib has.
## Selected references
- J. W. Cannon, W. J. Floyd, W. R. Parry, *Introductory notes on Richard Thompson's groups*,
L'Enseignement Mathématique (2) **42** (1996), 215–256.
[doi:10.5169/seals-87877](https://doi.org/10.5169/seals-87877)
- M. G. Brin, C. C. Squier, *Groups of piecewise linear homeomorphisms of the real line*,
Inventiones Mathematicae **79** (1985), 485–498.
[doi:10.1007/BF01388519](https://doi.org/10.1007/BF01388519)
- C. Chou, *Elementary amenable groups*, Illinois Journal of Mathematics **24** (1980), 396–407.
[doi:10.1215/ijm/1256047608](https://doi.org/10.1215/ijm/1256047608)
- M. M. Day, *Amenable semigroups*, Illinois Journal of Mathematics **1** (1957), 509–544.
[doi:10.1215/ijm/1255380675](https://doi.org/10.1215/ijm/1255380675)
- J. von Neumann, *Zur allgemeinen Theorie des Maßes*, Fundamenta Mathematicae **13** (1929),
73–116. [doi:10.4064/fm-13-1-73-116](https://doi.org/10.4064/fm-13-1-73-116)
- A. Yu. Olshanskii, *On a geometric method in the combinatorial group theory*, Proceedings of
the International Congress of Mathematicians (Warsaw, 1983), vol. 1, 1984, pp. 415–424.
[IMU archive](https://www.mathunion.org/fileadmin/ICM/Proceedings/ICM1983.1/ICM1983.1.ocr.pdf)
- M. Gromov, *Hyperbolic groups*, in *Essays in Group Theory* (S. M. Gersten, ed.), MSRI
Publications **8**, Springer, 1987, pp. 75–263.
[doi:10.1007/978-1-4613-9586-7_3](https://doi.org/10.1007/978-1-4613-9586-7_3)
Formalized SCOPE and REACH estimatorsResearch Paper
## Motivation
A _foundation model_ trained on tokenized electronic health record (EHR) timelines can be used to predict clinical outcomes without ever being finetuned for a specific prediction task: condition the model on a patient's observed timeline, autoregressively sample many possible futures, and report the fraction of sampled futures in which the outcome of interest occurs. This _generative approach_ to inference powers a growing family of EHR foundation models— including Event Stream GPT
([McDermott et al., 2023](https://arxiv.org/abs/2306.11547)), Foresight
([Kraljevic et al., 2024](https://doi.org/10.1016/S2589-7500%2824%2900025-6)),
ETHOS ([Renc et al., 2024](https://doi.org/10.1038/s41746-024-01235-0)),
and Curiosity ([Waxler et al., 2025](https://arxiv.org/abs/2508.12104))—and it is attractive for its zero-shot approach to predicting a variety of outcomes.
It is also expensive. Reproducing one published pipeline required more
than $1500$ A100 GPU-hours of inference. Worse, the estimator built from $n$ sampled futures
takes values in $\{0, 1/n, \dots, 1\}$, so its resolution is tied to the sampling budget: for
an outcome of prevalence $1/10{,}000$, $100$ sampled futures fail more than $90\%$ of the time
to rank a patient at ten times average risk above an average one. The most consequential
clinical decisions turn on exactly such low-prevalence, high-impact outcomes.
[Solo et al. (arXiv:2602.03730)](https://arxiv.org/abs/2602.03730) observe that Monte Carlo
discards almost everything the model produces: at every step the model emits a full next-token
distribution and the sampler keeps only the token it drew. The paper introduces two estimators
that consume the discarded probabilities instead, and proves that doing so costs no bias and—for one of them—never costs variance.
## Setting and estimators
Let $P$ generate token sequences from a countable vocabulary $V$, with designated outcome token $O$. The next-token probabilities may depend on the complete preceding history. The time threshold is initially unexceeded. Its crossing may depend on several kinds of time-spacing tokens and on their accumulated duration.
For a sampled timeline $X$, $T_O(X)$ is the first position occupied by $O$, or $\infty$ if it never appears. The time $T_E(X)$ is the first position at which the threshold has been exceeded. Assume $T_O\ne T_E$ almost surely. Timelines are retained through the actual threshold crossing, even if the outcome appears earlier. Thus $T_E$ is not reassigned after an outcome.
The threshold is reached almost surely, but the number of tokens required may be arbitrarily large. No deterministic bound or finite expected token count is assumed. For REACH, assume also that removing the outcome token and renormalizing defines a sampler that reaches the same threshold almost surely.
For $n\ge1$ independent original timelines, the **Monte Carlo estimator** is
$$M_0=\frac1n\sum_{i=1}^n 1_{\{T_O(X^{(i)})<T_E(X^{(i)})\}}.$$
The **SCOPE estimator** is
$$\mathcal S=\frac1n\sum_{i=1}^n\sum_{t=1}^{\min\{T_E(X^{(i)}),T_O(X^{(i)})\}}P(X_t=O\mid X_{1:t-1}^{(i)}).$$
For **REACH**, sample independent outcome-free timelines by setting the next-token probability of $O$ to zero and renormalizing the probabilities of the other tokens. Using the original model probabilities along those timelines, define
$$\mathcal R=\frac1n\sum_{i=1}^n\left[1-\prod_{t=1}^{T_E(\hat X^{(i)})}\left(1-P(X_t=O\mid\hat X_{1:t-1}^{(i)})\right)\right].$$
## Formalization targets
The targets are:
1. **SCOPE unbiasedness:** $\mathbb E[\mathcal S]=P(T_O<T_E)$.
2. **Equal probabilities milestone:** $P(A)=P(B)$ from Appendix C, where $A$ is the original outcome-before-threshold event and $B$ is at least one successful Bernoulli trial along an outcome-free timeline.
3. **REACH unbiasedness:** $\mathbb E[\mathcal R]=P(T_O<T_E)$.
4. **Rao–Blackwell identity:** for every positive sample count, conditioning the average of the two-stage event indicators on the entire pool of outcome-free timelines equals $\mathcal R$ almost surely.
5. **Main goal:** $\operatorname{Var}(\mathcal R)\le\operatorname{Var}(M_0)$ at the same positive sample count, with finite second moments for both estimators.
Expectations and variances use each estimator's specified sampling law.
## What the formalization establishes
The claims concern the probability assigned by the generative model. They provide unbiasedness and a comparison of sampling variance. SCOPE is kept unclipped, as in the paper's unbiasedness result. All five target statements have accompanying local Lean proofs.
## Main mathematical difficulty
A pathwise finite stopping time need not have a common finite bound or a finite mean. An expectation involving the stopped SCOPE sum therefore needs justification beyond finite-sum linearity. REACH uses a different sampling law, so its unbiasedness and variance comparison also require a proved connection between the original event and the two-stage experiment. The equal-probabilities milestone records that connection explicitly.
## Formalization scope
Lean represents each sampled timeline by a finite list ending at its first threshold crossing. Arbitrary finite lengths are included in the same sample space. Path probabilities are products of next-token probabilities, and the laws are countable sums of these path masses. Requiring each law to have total mass one expresses almost-sure termination of that sampler; it is not a uniform length bound. The vocabulary can be finite or countably infinite.
The stopping predicate examines a complete prefix and is not restricted to a single terminal token. The original law continues through outcomes until the threshold. A separate almost-everywhere hypothesis excludes equal outcome and threshold times. The code proves that the actual threshold time is finite almost surely and that the strict event $T_O<T_E$ is the event used by the internal calculations.
The two-stage experiment explicitly samples conditionally independent Bernoulli trials using the original hazards. Its conditioning information retains the complete indexed pool of outcome-free timelines. The Rao–Blackwell target uses Mathlib's conditional expectation. The variance target uses Mathlib's variance, and proves square integrability rather than assuming it.
## Selected references
- Luke Solo, Matthew B. A. McDermott, William F. Parker, Bashar Ramadan, Michael C. Burkhart, Brett K. Beaulieu-Jones, *Efficient Generative Prediction for EHR Foundation Models: The SCOPE and REACH Estimators*, 2026. [arXiv:2602.03730](https://arxiv.org/abs/2602.03730)
- M. B. A. McDermott, B. Nestor, P. Argaw, I. S. Kohane, *Event Stream GPT: A Data Pre-processing and Modeling Library for Generative, Pre-trained Transformers over Continuous-time Sequences of Complex Events*, Advances in Neural Information Processing Systems 36, pp. 24322–24334, 2023. [arXiv:2306.11547](https://arxiv.org/abs/2306.11547)
- Z. Kraljevic, D. Bean, A. Shek, R. Bendayan, H. Hemingway, J. A. Yeung, A. Deng, A. Baston, J. Ross, E. Idowu, J. T. Teo, R. J. B. Dobson, *Foresight—a generative pretrained transformer for modelling of patient timelines using electronic health records: a retrospective modelling study*, Lancet Digital Health 6(4), pp. e281–e290, 2024. [doi:10.1016/S2589-7500(24)00025-6](https://doi.org/10.1016/S2589-7500%2824%2900025-6)
- P. Renc, Y. Jia, A. E. Samir, J. Was, Q. Li, D. W. Bates, A. Sitek, *Zero shot health trajectory prediction using transformer*, npj Digital Medicine 7(1), p. 256, 2024. [doi:10.1038/s41746-024-01235-0](https://doi.org/10.1038/s41746-024-01235-0)
- S. Waxler, P. Blazek, D. White, D. Sneider, K. Chung, M. Nagarathnam, P. Williams, H. Voeller, K. Wong, M. Swanhorst, S. Zhang, N. Usuyama, C. Wong, T. Naumann, H. Poon, A. Loza, D. Meeker, S. Hain, R. Shah, *Generative medical event models improve with scale*, 2025. Introduces the Curiosity model family. [arXiv:2508.12104](https://arxiv.org/abs/2508.12104)
## Motivation
Almost every classical transcendence theorem is a statement about the interaction between the additive structure of $\mathbb{C}$ and the exponential function. Hermite proved in 1873 that $e$ is transcendental, Lindemann in 1882 that $e^{\alpha}$ is transcendental for every nonzero algebraic $\alpha$ — hence that $\pi$ is transcendental and the circle cannot be squared — and Weierstrass in 1885 extended this to the linear independence of $e^{\alpha_1},\dots,e^{\alpha_n}$ over $\overline{\mathbb{Q}}$ for distinct algebraic $\alpha_i$. Gelfond and Schneider settled Hilbert's seventh problem in 1934, and Baker's 1966 theorem on linear forms in logarithms made the subject effective.
**Schanuel's conjecture**, formulated by Stephen Schanuel in the 1960s and first published by Lang (*Introduction to Transcendental Numbers*, Addison–Wesley, 1966, Chapter III), is a single statement that contains all of these as special cases, together with a large number of statements that remain open — for instance that $e$ and $\pi$ are algebraically independent, or that $e + \pi$ is irrational. No case of it is known beyond those already covered by the Lindemann–Weierstrass theorem or by Baker's theorem.
Timeline, with the hypotheses each result actually assumes:
- 1882, Lindemann: $e^{\alpha}$ is transcendental for algebraic $\alpha \neq 0$.
- 1885, Weierstrass: for pairwise distinct algebraic $\alpha_1,\dots,\alpha_n$, the values $e^{\alpha_1},\dots,e^{\alpha_n}$ are linearly independent over $\overline{\mathbb{Q}}$.
- 1934, Gelfond and Schneider, independently: if $\lambda \neq 0$ is a logarithm of an algebraic number and $\beta$ is algebraic and irrational, then $e^{\beta\lambda}$ is transcendental.
- 1960s, Siegel, Lang and Ramachandra: the six exponentials theorem, unconditional; the analogous four exponentials statement is still open.
- 1966, Baker: if logarithms $\lambda_1,\dots,\lambda_n$ of algebraic numbers are linearly independent over $\mathbb{Q}$, then $1,\lambda_1,\dots,\lambda_n$ are linearly independent over $\overline{\mathbb{Q}}$.
- 1971, Ax: the function-field analogue of Schanuel's conjecture, for formal power series and, more generally, differential fields of characteristic zero.
## Setting
Write $\exp$ for the complex exponential function. A tuple $z_1,\dots,z_n$ of complex numbers is **linearly independent over $\mathbb{Q}$** when the only rationals $q_1,\dots,q_n$ with $\sum_i q_i z_i = 0$ are $q_1 = \dots = q_n = 0$; here $\mathbb{C}$ is viewed as a vector space over $\mathbb{Q}$.
For a subset $S \subseteq \mathbb{C}$, let $\mathbb{Q}(S)$ denote the subfield of $\mathbb{C}$ generated by $S$ over $\mathbb{Q}$. The **transcendence degree** $\operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}(S)$ is the cardinality of a transcendence basis of $\mathbb{Q}(S)$ over $\mathbb{Q}$: the largest number of elements of $\mathbb{Q}(S)$ that are algebraically independent over $\mathbb{Q}$. A number $x$ is **transcendental** over $\mathbb{Q}$ when no nonzero polynomial with rational coefficients vanishes at $x$, and numbers $x_1,\dots,x_m$ are **algebraically independent** over $\mathbb{Q}$ when no nonzero polynomial in $m$ variables with rational coefficients vanishes at $(x_1,\dots,x_m)$.
## Formalization targets
### Goal
$$z_1,\dots,z_n \text{ linearly independent over } \mathbb{Q} \;\Longrightarrow\; \operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}\bigl(z_1,\dots,z_n,\,e^{z_1},\dots,e^{z_n}\bigr) \;\ge\; n .$$
The goal fixes no numerical constant and no special shape for the $z_i$: it asserts only the inequality, for every $n$ and every $\mathbb{Q}$-linearly independent tuple. The case $n = 0$ is vacuous and the conclusion is a bound on a cardinal, so nothing is hidden in a degenerate convention.
### Milestones
The milestone list consists of the landmark unconditional theorems that Schanuel's conjecture generalizes, the known function-field analogue, and one conditional corollary that records what the conjecture buys:
- Hermite–Lindemann (1882): $\alpha$ algebraic and nonzero $\Rightarrow$ $e^{\alpha}$ transcendental.
- Lindemann–Weierstrass (1885): $\sum_i \beta_i e^{\alpha_i} \neq 0$ for distinct algebraic $\alpha_i$ and algebraic $\beta_i$ not all zero.
- Gelfond–Schneider (1934): $\lambda \neq 0$ a logarithm of an algebraic number, $\beta$ algebraic irrational $\Rightarrow$ $e^{\beta\lambda}$ transcendental.
- Six exponentials theorem: $x_1,x_2$ and $y_1,y_2,y_3$ each $\mathbb{Q}$-linearly independent $\Rightarrow$ at least one of the six numbers $e^{x_i y_j}$ is transcendental.
- Baker (1966): $\mathbb{Q}$-linearly independent logarithms of algebraic numbers, together with $1$, are linearly independent over $\overline{\mathbb{Q}}$.
- Ax (1971), power series form: $\operatorname{trdeg}_{\mathbb{C}} \mathbb{C}(f_1,\dots,f_n,g_1,\dots,g_n) \ge n+1$ when $g_i' = f_i' g_i$, the $g_i$ are units, and no nontrivial $\mathbb{Q}$-linear combination of the $f_i$ is constant.
- Conditional corollary: Schanuel's conjecture implies that $e$ and $\pi$ are algebraically independent over $\mathbb{Q}$.
## Significance
Schanuel's conjecture decides, in one stroke, a long list of questions that are individually open: the algebraic independence of $e$ and $\pi$, the irrationality of $e+\pi$ and of $e\pi$, the transcendence of $e^{e}$ and $\pi^{\pi}$, the four exponentials conjecture, and — combined with work of Macintyre and Wilkie — the decidability of the first-order theory of the real exponential field. Its restriction to algebraic $z_i$ is exactly the Lindemann–Weierstrass theorem, and its restriction to $z_i$ whose exponentials are algebraic is exactly Baker's theorem, so the conjecture is a common generalization of the two main unconditional pillars of the subject.
On the formalization side, the state of the art in Lean's mathematical library is modest relative to this history: the analytic core of the Lindemann–Weierstrass argument is present, but the Hermite–Lindemann theorem, the Lindemann–Weierstrass theorem, the transcendence of $\pi$, the Gelfond–Schneider theorem, the six exponentials theorem and Baker's theorem are not available as usable statements in the pinned environment. Each milestone here is therefore a genuine formalization project with a known mathematical proof, and none of them is a restatement of an existing library result. The goal theorem itself is open mathematically; the realistic contributions to it are reductions — implications between the goal and other statements — and closing the milestones that the conjecture generalizes.
## Difficulty
The obvious approach to any single case — build an auxiliary function with many zeros, bound its derivatives, and derive a contradiction from an integrality argument — is the method behind every result on the milestone list, and it is exactly what fails for the conjecture in general. Those proofs need the exponentials, or the arguments, to be algebraic somewhere, so that heights and denominators can be controlled; for a general $\mathbb{Q}$-linearly independent tuple there is no arithmetic input at all, and no known construction produces the required auxiliary function. Ax's theorem shows that the differential-algebraic shadow of the statement is true, but its proof uses the derivation on the function field and has no arithmetic counterpart. A solver should not expect the conjecture itself to fall to a variation of the classical method.
## Formalization scope
All statements are over $\mathbb{C}$, with the complex exponential. Tuples are indexed by `Fin n`, `ℚ`-linear independence is Mathlib's `LinearIndependent ℚ`, transcendence degree is Mathlib's `Algebra.trdeg`, the generated field is `IntermediateField.adjoin`, and the inequality is between cardinals, so the goal reads `(n : Cardinal) ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z)))`. Algebraicity is `IsAlgebraic ℚ`, transcendence is `Transcendental ℚ`, and algebraic independence is `AlgebraicIndependent ℚ`.
There is no trivializing formalization here: the hypothesis `LinearIndependent ℚ z` is satisfiable for every $n$, so the goal is not vacuous, and the conclusion is an inequality of cardinals rather than a statement about a definition introduced for this mission.
The Ax milestone is stated for formal power series in one variable over $\mathbb{C}$: the exponential relation is expressed as the differential equation $g_i' = f_i' g_i$ with `PowerSeries.derivative`, and the conclusion bounds `Algebra.trdeg ℂ` of the `ℂ`-subalgebra generated by the $f_i$ and the $g_i$. The conditional corollary takes the full statement of Schanuel's conjecture as an explicit hypothesis, so it is provable unconditionally as stated.
Infrastructure that a complete development needs, and that is reusable well beyond this mission: Siegel's lemma and height machinery for algebraic numbers, the standard auxiliary-function construction with derivative bounds, and interface lemmas relating `Algebra.trdeg`, `AlgebraicIndependent` and `Transcendental`. Reductions between the milestones — for example deriving Hermite–Lindemann from Lindemann–Weierstrass, or the six exponentials theorem from a general Baker-type statement — are welcome as sketches.
## Selected references
- S. Lang, *Introduction to Transcendental Numbers*, Addison–Wesley, 1966. (Schanuel's conjecture is stated in Chapter III.)
- A. Baker, *Linear forms in the logarithms of algebraic numbers I*, Mathematika 13 (1966), 204–216. https://doi.org/10.1112/S0025579300003971
- J. Ax, *On Schanuel's conjectures*, Annals of Mathematics 93 (1971), 252–268. https://doi.org/10.2307/1970774
- A. Macintyre and A. J. Wilkie, *On the decidability of the real exponential field*, in Kreiseliana, A K Peters, 1996, 441–467.
- M. Waldschmidt, *Diophantine Approximation on Linear Algebraic Groups*, Springer, 2000.
- Wikipedia, *Schanuel's conjecture*. https://en.wikipedia.org/wiki/Schanuel%27s_conjecture
## Motivation
Write the primes in increasing order, take the absolute differences of consecutive
entries, take the absolute differences of the resulting row, and repeat. Every row
produced this way appears to begin with $1$:
$$
\begin{array}{llllllll}
2 & 3 & 5 & 7 & 11 & 13 & 17 & \dots\\
1 & 2 & 2 & 4 & 2 & 4 & \dots\\
1 & 0 & 2 & 2 & 2 & \dots\\
1 & 2 & 0 & 0 & \dots\\
1 & 2 & 0 & \dots
\end{array}
$$
**Gilbreath's conjecture** asserts that this never fails. The observation is due to
Norman L. Gilbreath (1958), who rediscovered a statement already published by
François Proth in 1878 together with an argument that is not accepted as a proof.
It is attractive because it is elementary to state and because it is one of the few
statements about the primes whose difficulty is not visibly analytic: it concerns the
combinatorics of iterated differences rather than the distribution of primes directly.
*Timeline.*
- 1878 — **Proth** states the property and publishes a proof that is now regarded as
erroneous.
- 1958 — **Gilbreath** rediscovers the pattern; it circulates as a conjecture.
- 1959 — **Killgrove and Ralston** verify the leading entry for the first $63{,}418$
rows ([MTAC 13 (1959), 121–122](https://doi.org/10.1090/S0025-5718-1959-0105398-3)).
- 1993 — **Odlyzko** reports a verification of the leading entry for all rows of index
at most $\pi(10^{13}) \approx 3.4 \times 10^{11}$, using an argument that propagates a
long block of entries lying in $\{0,2\}$ downwards through the triangle
([Math. Comp. 61 (1993), 373–380](https://doi.org/10.1090/S0025-5718-1993-1192979-9)).
No proof is known.
## Setting
Let $p_0 = 2 < p_1 = 3 < p_2 = 5 < \dots$ be the increasing enumeration of the prime
numbers, indexed from $0$. Define the rows of the **Gilbreath triangle** by
$$
d^0(n) = p_n, \qquad d^{k+1}(n) = \bigl| d^{k}(n+1) - d^{k}(n) \bigr| \quad (k, n \ge 0).
$$
Thus $d^k$ is an infinite sequence of natural numbers for every $k$, row $0$ is the
sequence of primes, row $1$ is the sequence of prime gaps $p_{n+1}-p_n$, and each
later row is the sequence of absolute differences of consecutive entries of the row
above it. Only the leading entry $d^k(0)$ of each row is at issue.
More generally, for an arbitrary sequence $a : \mathbb{N} \to \mathbb{N}$ write
$(\Delta a)(n) = |a(n+1) - a(n)|$ and $\Delta^j a$ for the $j$-fold iterate, so that
$d^k = \Delta^k p$.
## Formalization targets
### Goal
$$
\forall k \ge 1,\qquad d^{k}(0) = 1 .
$$
This is the conjecture in its standard form: every row after the row of primes begins
with $1$. It fixes no constants and no ranges, so no computational advance can
invalidate it.
### Milestones
The milestone list collects the statements that a proof, or a further computational
verification, would be built from: the two low-level structural facts about the
triangle (row $1$ is the gap sequence; from row $1$ on, the leading entry is odd and
all later entries are even), a finite verification of the first rows, and the two
statements underlying Odlyzko's method — the propagation lemma for an arbitrary
sequence beginning $1$ and continuing in $\{0,2\}$, and the reduction of the
conjecture to the existence, for each row index, of an earlier row with a long enough
block of entries in $\{0,2\}$.
## Significance
*The result itself.* The conjecture is not known to imply other open statements about
the primes, and its interest lies elsewhere: it is a test case for how much of the
fine structure of the prime sequence is forced by coarse information. The propagation
mechanism shows that the conjecture for a given row index follows from purely local
data about an earlier row, and that mechanism is what every verification to date has
relied on. A proof would have to show that such blocks of entries in $\{0,2\}$ always
appear early enough, which is a statement about the density of small prime gaps in
disguise.
*Formalizing it.* Nothing here is currently formalized: Mathlib has the prime
enumeration $n \mapsto p_n$ (`Nat.nth Nat.Prime`) and the basic facts about it, but
not the iterated-difference triangle nor any of its properties. This mission
contributes the definition of the triangle, the structural facts about its rows, and
a machine-checked version of the reduction step that all computational work on the
problem uses. The goal theorem itself is open — the milestones are known mathematics,
and each is provable with current tools, while the goal is not.
## Difficulty
The obvious attack is induction on the row index: to see that $d^{k+1}(0) = 1$ it
suffices to know that $d^{k}(0) = 1$ and $d^{k}(1) \in \{0,2\}$. But controlling
$d^{k}(1)$ requires controlling $d^{k-1}(1)$ and $d^{k-1}(2)$, and so on: the
invariant that closes is not "the row begins with $1$" but "the row begins with $1$
and its next $m$ entries lie in $\{0,2\}$", and each application of the difference
operator consumes one entry of that block. So a finite block of good entries only
carries the conclusion a finite number of rows further down, and the conjecture needs
such blocks to keep reappearing forever, arbitrarily far down the triangle. Nothing is
known that produces them.
A second warning, due to Hallard Croft: the property is not specific to the primes.
Sequences that start with $2$, continue with odd numbers, and have gaps that are not
too large empirically exhibit the same behaviour, so any proof that uses only such
coarse features would prove a much more general statement — and conversely, an
argument exploiting deep properties of primes is likely to be proving the wrong thing.
## Formalization scope
Rows are total functions $\mathbb{N} \to \mathbb{N}$, defined for every index, and the
whole triangle is a single family indexed by the row number. Differences are taken as
`Int.natAbs` of a difference computed in $\mathbb{Z}$, so truncated natural
subtraction never occurs; the one place where $\mathbb{N}$-subtraction does appear is
the milestone identifying row $1$ with the gap sequence, where the subtraction is
justified by monotonicity of $n \mapsto p_n$.
Primes are indexed from $0$ via Mathlib's `Nat.nth Nat.Prime`, so $p_0 = 2$; rows are
indexed with row $0$ the primes, and the goal quantifies over all $k \ge 1$ in the
form `d (k + 1) 0 = 1`, with no upper bound and no extra hypothesis, so no vacuous or
finitely-truncated reading of the goal is available. The general difference operator
is stated for arbitrary sequences $\mathbb{N} \to \mathbb{N}$, which is what makes the
propagation lemma usable as a black box, and reusable beyond this mission.
A complete development needs no analytic input for the milestones: Mathlib's
`Nat.nth`, `Nat.prime_nth_prime`, `Nat.nth_prime_zero_eq_two` and the strict
monotonicity of the prime enumeration suffice. Contributions that would extend the
mission beyond its current list: a formal version of a concrete computational
verification (checking that the leading entries of the first $N$ rows are $1$ for an
$N$ well beyond the hand-checkable range), and formalizations of the general
statement for non-prime sequences of the Croft type.
## Selected references
- N. L. Gilbreath, as reported in R. B. Killgrove and K. E. Ralston, *On a conjecture
concerning the primes*, Mathematical Tables and Other Aids to Computation 13 (1959),
121–122. https://doi.org/10.1090/S0025-5718-1959-0105398-3
- A. M. Odlyzko, *Iterated absolute values of differences of consecutive primes*,
Mathematics of Computation 61 (1993), 373–380.
https://doi.org/10.1090/S0025-5718-1993-1192979-9
- Gilbreath's conjecture, Wikipedia. https://en.wikipedia.org/wiki/Gilbreath%27s_conjecture
Fading Memory and Approximation of Nonlinear Operators (Boyd & Chua, 1985)Research Paper
## Motivation
A recurrent network, a nonlinear filter, a physical transducer: all are **operators** carrying an input signal to an output signal. Approximating such an operator — not a function on $\mathbb{R}^n$, but a map between signal spaces — is the question behind every claim that a recurrent architecture is "universal".
In 1985 Boyd and Chua gave the answer that still underpins the field. They isolated **fading memory** as the exact continuity notion required, and proved that a time-invariant operator with fading memory can be approximated by a finite Volterra series — uniformly over an **infinite time horizon** and over a **noncompact** set of signals. Both italicised words mark the break with what was available before: the classical Volterra approximation theorems hold only on a finite interval $[0,T]$ and only on a compact set of inputs, which rules out most signals of engineering interest.
This is the result reservoir computing inherits. Every modern universality theorem for echo state networks, state-affine systems, or linear-dynamics-plus-polynomial-readout architectures proceeds by showing the architecture realises enough of these operators, then invokes Boyd–Chua. Formalising it turns the foundation of those arguments into machine-checked mathematics.
**Timeline.**
- 1958 — Volterra series are the standard tool for weakly nonlinear systems, but the available approximation theorems are confined to a finite interval and a compact input set.
- 1985 — Boyd and Chua identify fading memory and remove both restrictions. Theorem 1 is the continuous-time statement; Theorems 3 and 4 are its discrete-time counterparts.
- 2001 — Jaeger introduces echo state networks; the echo state property is the well-posedness half of the same picture.
- 2018 — Grigoryeva and Ortega prove universality for reservoir computers by reducing to Boyd–Chua.
## Setting
Following the convention of the published `ReservoirESN` definitions, **the index counts steps into the past**: $u_k$ (discrete) or $u(t)$ (continuous) is the value of the signal $k$ steps, or $t$ units of time, *before* the present. A sequence or function is therefore the complete history of a signal up to now. Under this convention every operator below is causal.
A **weighting** is a map $w$ decreasing to zero with values in $(0,1]$, and the **weighted norm** is $\lVert u \rVert_w = \sup_{t \ge 0} \lvert u(t)\rvert\, w(t)$ — the distant past is discounted.
An operator $N$ is **time-invariant** when its value at any instant is its present-time value applied to the shifted history, $(Nu)(r) = \big(N(\sigma^r u)\big)(0)$ with $(\sigma^r u)(t) = u(t+r)$. It has **fading memory** on a set $K$ when its present-time functional $u \mapsto (Nu)(0)$ is $\lVert\cdot\rVert_w$-continuous on $K$. The quantifier order is taken verbatim from the source: $\delta$ may depend on the input $u$ as well as on $\varepsilon$, so this is *pointwise* continuity — formally weaker than the uniform version `ReservoirESN.FunctionalFMP` already on the platform.
In continuous time the admissible inputs are the **bounded, slew-limited** signals
$$ K = \{\, u \;:\; \lvert u(t)\rvert \le M_1,\quad \lvert u(s)-u(t)\rvert \le M_2\,\lvert s-t\rvert \,\}, $$
and the approximating functionals are the **convolutions** $G_g u = \int_0^\infty g(t)\,u(t)\,dt$ with $\int_0^\infty \lvert g\rvert/w < \infty$.
## Goal — Theorem 1
> Let $\varepsilon > 0$ and let $N$ be any time-invariant operator with fading memory on $K$. Then there are finitely many admissible kernels $g_1,\dots,g_m$ and a polynomial $p : \mathbb{R}^m \to \mathbb{R}$ such that
> $$ \sup_{u \in K}\ \sup_{r \ge 0}\ \Big\lvert (Nu)(r) - p\big(G_{g_1}\sigma^r u,\ \dots,\ G_{g_m}\sigma^r u\big) \Big\rvert \ \le\ \varepsilon. $$
That is: **a bank of linear filters followed by a polynomial readout** — the architecture of Fig. 3 of the paper, and, recognisably, the architecture of a reservoir computer. The goal is stated in this form rather than as an explicit Volterra kernel expansion; expanding a polynomial in convolutions into Volterra kernels is a purely algebraic restatement, and formalising Volterra kernels would add bookkeeping without adding mathematical content. The approximation is uniform over all of $K$ at once and over all time at once, and $K$ is **not** compact in the sup norm — the whole point of fading memory is that it makes $K$ behave as though it were.
## Milestones
The decomposition follows the paper: the discrete-time chain first (Section VI and Appendix A2), then the two continuous-time lemmas the goal rests on (Section IV and Appendix A1).
**1 — Damping, and compactness of the discrete ball.** On the $\ell^\infty$ ball, closeness over a finite horizon already forces closeness in weighted norm; consequently the weighted topology and the product topology coincide there, and the ball is compact by Tychonoff. This is the discrete analogue of Lemma A1, and the only place where $w \to 0$ is used.
**2 — Theorem 4, the discrete NLMA approximation.** Fading memory becomes topological continuity on that compact ball; the delay functionals $u \mapsto u_k$ separate points; Stone–Weierstrass then yields a **nonlinear moving average** — a polynomial read from a finite window, $(\widehat{N}u)_k = p(u_k,\dots,u_{k+m-1})$ — approximating $N$ uniformly. Boyd and Chua note this implies Theorem 3, the discrete finite-Volterra statement.
**3 — Lemma 1: compactness in continuous time.** The bounded slew-limited set is compact for the weighted norm. The source proves it by Arzelà–Ascoli on each interval $[-n,0]$ followed by a diagonal extraction; the slew limit is exactly the equicontinuity that makes this work, and it is *required* here — the discrete case needs no analogue, as the paper remarks.
**4 — Lemma 2: the convolution functionals separate points.** Admissible kernels give $\lVert\cdot\rVert_w$-continuous functionals, and they separate: for $u \neq v$ the kernel $g_0(t) = (u(t)-v(t))\,w(t)\,e^{-t}$ is admissible and $G_{g_0}u - G_{g_0}v = \int_0^\infty (u-v)^2 w\, e^{-t} > 0$.
**Goal.** Stone–Weierstrass on the compact set of milestone 3 with the separating family of milestone 4, then time-invariance to transport the estimate to every instant.
## What is already available
The companion missions on reservoir computing have published, machine-checked, the definitions reused here — `UnifBdd`, `WeightedBound`, `IsWeighting`, `FunctionalFMP` — along with `WeightedCompact.unifBdd_tendsto_subseq`, a weighted sequential-compactness result for the discrete ball. Solvers can build on those rather than restate them.
## Why this is not routine
Mathlib has Stone–Weierstrass in the form needed (`ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints`, which asks only for `CompactSpace`), and it has Arzelà–Ascoli in an abstract uniform-space form. What it has **nothing** about is fading memory, weighted norms on signal spaces, Volterra series, Laguerre systems, or moving-average operators. The work is the bridge: turning a weighted-norm continuity hypothesis into a topological statement Mathlib's Stone–Weierstrass will accept, extracting a genuine `MvPolynomial` from an abstract density result, and — for the goal — assembling a compactness proof in continuous time from Mathlib's Ascoli machinery.
Two modelling points are load-bearing and stated plainly rather than buried. The discrete ball must be taken in scalar (or finite-dimensional) signals: for infinite-dimensional values it is not compact and the theorem fails. And in continuous time the slew limit cannot be dropped: without equicontinuity the set is not compact in any topology that makes the convolution functionals continuous.
## Source
S. Boyd and L. O. Chua, *Fading memory and the problem of approximating nonlinear operators with Volterra series*, IEEE Transactions on Circuits and Systems, vol. CAS-32, no. 11, pp. 1150–1161, November 1985.
## Motivation
Transformer sequence models modulate attention scores by a function of the relative
position between a query and a key: the attention logit between token $m$ and token
$n$ is scaled by a fixed profile $f(p_m - p_n)$. Realizing this modulation the naive
way means evaluating $f$ once per pair $(m,n)$ and materializing an $L\times L$
adjustment over the whole sequence — quadratic in the sequence length $L$. Rotary
Position Embedding (RoPE) [Su et al. 2021](https://arxiv.org/abs/2104.09864) avoids
this entirely: it rotates the query at position $p_m$ and the key at position $p_n$
*independently*, each by an angle depending only on its own position, so that the
pairwise quantity $f(p_m-p_n)$ falls out of the dot product of the two separately
rotated vectors — $f$ is never evaluated pairwise, and no $L\times L$ matrix is ever
built. This is what lets RoPE stay a linear, per-token preprocessing step compatible
with efficient (sub-quadratic) attention implementations, rather than an $O(L^2)$
modulation. The catch is that RoPE's specific log-linear frequency schedule bakes in
one particular profile: a monotone, decaying $f$. That schedule is a poor fit
whenever the correlation structure of the data is not monotonically decaying with
distance — the leading example being **periodicity**: in sequential recommendation,
interactions separated by exactly one day or one week are more correlated than
interactions separated by, say, half a day, and a decaying profile cannot express
that "attention comes back" at the period.
Chen, Ainslie, Choromanski et al., *ClockRoPE: Random Fourier Rotations for Temporal
Routine Modeling* ([arXiv:2607.26369](https://arxiv.org/abs/2607.26369)), ask a more
general question first: which attention-modulation profiles $f$ can be realized *at
all* by this same per-token, pairwise-iteration-free rotation trick — rotate each
token once, on its own, and let the pairwise profile emerge from the dot product —
and by what rotation-frequency schedule? Their answer is a random-features
construction — sample the rotation frequencies from the kernel's own Fourier
transform, rather than fixing them log-linearly — that realizes *any* continuous,
normalized, positive-definite profile in expectation, with a quantified concentration
rate, all while keeping the exact same per-token rotate-then-dot-product computation
RoPE already uses. ClockRoPE is the periodic instance of this general theory, later
deployed in a production-scale generative-retrieval system.
## Setting
Fix an embedding dimension $d = 2n$ and group a vector $v \in \mathbb{R}^d$ into $n$
consecutive **feature pairs** $v^{(j)} = (v_{2j}, v_{2j+1}) \in \mathbb{R}^2$ for
$j = 0, \dots, n-1$. For an angle $\theta$, let
$$
R(\theta) = \begin{pmatrix} \cos\theta & -\sin\theta \\ \sin\theta & \cos\theta \end{pmatrix}
$$
be the $2\times 2$ (Givens) rotation matrix. A real kernel $f : \mathbb{R} \to
\mathbb{R}$ is **positive definite** if for every finite family of points
$x_1,\dots,x_N \in \mathbb{R}$ and complex coefficients $c_1,\dots,c_N$,
$\sum_{i,j} \overline{c_i} c_j f(x_i - x_j)$ has nonnegative real part; it is
**normalized** if $f(0) = 1$. When $f$ is also continuous and Lebesgue-integrable,
its Fourier transform
$$
\tau(\xi) = \int_{\mathbb{R}} f(x) e^{-i2\pi\xi x}\,dx
$$
is (by Bochner's theorem) a genuine probability density on $\mathbb{R}$: this is the
distribution the mission's rotation frequencies are sampled from.
Given a query $q_m \in \mathbb{R}^{2n}$ at position $p_m$, a key $k_n \in
\mathbb{R}^{2n}$ at position $p_n$, and $n$ i.i.d. frequencies $\xi_0, \dots,
\xi_{n-1} \sim \tau$, the **Random Fourier Rotation (RFR) estimator** is
$$
\hat g(q_m, k_n, p_m, p_n) = \sum_{j=0}^{n-1} \big(R(2\pi\xi_j p_m)\, q_m^{(j)}\big)^\top \big(R(2\pi\xi_j p_n)\, k_n^{(j)}\big).
$$
$\hat g$ is exactly the modulated attention logit computed by rotating query/key
feature pairs with per-pair, sampled RoPE frequencies — the same operation standard
RoPE performs, but with $\xi_j$ drawn from $\tau$ instead of fixed by a log-linear
schedule.
## Formalization targets
### Goal — convergence of the RFR estimator (Proposition 3.2)
$$
P\!\left(\left|\tfrac1n \hat g(q_m,k_n,p_m,p_n) - \tfrac1n\, q_m^\top k_n f(p_m-p_n)\right| \ge \epsilon\right)
\le 2\exp\!\left(-\frac{\epsilon^2(2n)^2}{8\sum_{j=0}^{n-1}\big(\lVert q_m^{(j)}\rVert\, \lVert k_n^{(j)}\rVert\big)^2}\right)
$$
for every $\epsilon > 0$. This is the mission's central target: it upgrades the mean
identity below into a quantitative, non-asymptotic guarantee that the sampled
estimator is close to the target profile with high probability, at a rate that is
exponential in the embedding dimension $d = 2n$.
### Milestone — unbiasedness of the RFR estimator (Proposition 3.1)
$$
\mathbb{E}_{\xi_0,\dots,\xi_{n-1}\sim\tau}\big[\hat g(q_m,k_n,p_m,p_n)\big] = q_m^\top k_n\, f(p_m-p_n).
$$
The expectation identity that the concentration bound above sharpens; it is the
feasibility half of the claim ("this construction is correct on average") that the
convergence half needs as its starting point.
### Milestone — periodic case via Herglotz's theorem (Corollary 3.3)
For a continuous, positive-definite, $T$-periodic $f$ with $f(0)=1$ and Fourier
coefficients $\alpha_k = \frac1T \int_0^T f(x) e^{-i2\pi kx/T}\,dx$,
$$
\alpha_k \ge 0 \text{ for all } k \in \mathbb{Z}, \qquad \sum_{k=-\infty}^{\infty} \alpha_k = f(0) = 1.
$$
The periodic specialization needed to apply the goal and first milestone with a
*discrete* frequency distribution over harmonics $k/T$ — the regime ClockRoPE
actually deploys, since daily/weekly routines are periodic rather than merely
decaying.
## Significance
The result gives a general recipe — sample, don't hand-design — for turning *any*
admissible attention-modulation profile into a RoPE-compatible rotation schedule,
with a concentration guarantee that says how many feature pairs are needed before the
sampled schedule reliably approximates the target profile. Crucially, the recipe
changes only *which frequencies* the per-token rotation uses — it never touches the
computational shape of RoPE itself: each query and key is still rotated once,
independently, by an angle depending only on its own position, and the target
pairwise profile $f(p_m-p_n)$ is still recovered purely from the dot product of the
two rotated vectors. So realizing an arbitrary positive-definite $f$ this way costs
exactly what realizing RoPE's own log-linear profile costs — linear in the sequence
length, with no pairwise evaluation of $f$ and no $L\times L$ matrix ever
materialized — rather than the quadratic cost a direct, per-pair implementation of
an arbitrary modulation function would require. This subsumes standard RoPE's
log-linear schedule as one instance and explains, via the periodic corollary, why a
schedule built from the kernel's own spectrum (rather than an arbitrary log-linear
one) is the right way to encode periodicity: nothing about the construction, or its
efficiency, is specific to decay. The paper reports this translated into measured
gains in a production-scale generative-retrieval system, which is unusual weight of
practical evidence behind a Bochner/Herglotz-style spectral argument.
At the time of writing, none of these three results have a machine-checked proof;
this mission asks for the first formalization of all three, together with the shared
scaffolding (feature-pair extraction, the rotation estimator, and the notion of a
positive-definite kernel) they are stated over.
## Difficulty
The natural first attempt at the concentration bound is a direct union bound or a
naive variance argument, but the estimator $\hat g$ is a sum of $n$ terms that are
each *bounded* (each rotated pair lies on a fixed-radius circle) rather than governed
by a variance bound that shrinks with $n$ under a fixed frequency; the source proof
instead applies McDiarmid's bounded-differences inequality, treating each sampled
frequency $\xi_j$ as one coordinate of the input and bounding the one-coordinate
change in $\hat g$ by $2\lVert q_m^{(j)}\rVert\lVert k_n^{(j)}\rVert$ via the
maximal distance between two points on the unit circle — not by directly bounding a
variance term. Establishing Proposition 3.1 itself already requires care: it
requires justifying that $\tau$, defined purely as an integral transform of $f$, is
in fact a legitimate probability density (Bochner's theorem), and then a real/complex
bookkeeping argument identifying the real inner product of rotated pairs with the
real part of a product of complex exponentials.
## Formalization scope
The mission works over the reals and represents feature pairs as functions
`Fin (2 * n) → ℝ` sliced into `Fin n`-indexed pairs, matching the "$n$ feature pairs,
dimension $d = 2n$" convention used throughout; $2\times2$ rotations are ordinary
`Matrix (Fin 2) (Fin 2) ℝ` values built with `Matrix.mulVec`/`Matrix.dotProduct`, and
expectation over i.i.d. $\tau$-distributed frequencies is formalized as integration
against the product measure `MeasureTheory.Measure.pi` of `n` independent copies of
the measure with density $\tau$ (`MeasureTheory.Measure.withDensity`) — this is
mathematically equivalent to, and more directly usable in Lean than, introducing an
abstract probability space with named i.i.d. random variables.
Since a general continuous positive-definite kernel need not have an
*integrable* Fourier transform (the periodic case in Corollary 3.3 is exactly the
counterexample: its "Fourier transform" is a discrete measure, not a density) — the
goal and first milestone add `Integrable f` as an explicit hypothesis beyond what the
paper states in prose, so that $\tau$ is genuinely a density rather than a junk value.
This is not a strengthening of the target profiles the paper cares about in practice
(Gaussian, Laplace, and the cosine/Gaussian priors used by ClockRoPE itself are all
integrable) and mirrors the paper's own split between the density case (Propositions
3.1–3.2) and the discrete, purely-periodic case (Corollary 3.3). A formalization that
dropped this hypothesis and instead let the Fourier integral silently evaluate to
Lean's junk value (`0` for non-integrable integrands) would make the goal statement
possible to "prove" vacuously and must be avoided.
Definitions needed: a positive-definite-kernel predicate, the real-valued Fourier
transform of a kernel, feature-pair extraction, the $2\times2$ rotation matrix, and
the RFR estimator itself — all reusable by any future mission formalizing RoPE-family
positional encodings (e.g. STRING, nD-RoPE) or other random-Fourier-feature results.
McDiarmid's inequality, if not already in Mathlib in the needed form, is itself a
independently reusable contribution.
## Selected references
- Yiwen Chen, Joshua Ainslie, Krzysztof Choromanski, Xiang Gao, Su-Lin Wu, Yiping Yuan, Qian Sun, *ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling*, 2026. [arXiv:2607.26369](https://arxiv.org/abs/2607.26369)
- Jianlin Su, Yu Lu, Shengfeng Pan, Ahmed Murtadha, Bo Wen, Yunfeng Liu, *RoFormer: Enhanced Transformer with Rotary Position Embedding*, arXiv, 2021. [arXiv:2104.09864](https://arxiv.org/abs/2104.09864)
- Ali Rahimi, Benjamin Recht, *Random Features for Large-Scale Kernel Machines*, NeurIPS, 2007.
- Salomon Bochner, *Monotone Funktionen, Stieltjessche Integrale und harmonische Analyse*, Springer, 1933.
- Gustav Herglotz, *Über Potenzreihen mit positivem, reellem Teil im Einheitskreis*, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.
The Monotonicity Theorem in O-Minimal Geometry 1: Monotonicity TheoremTextbook
## Motivation
An **o-minimal structure** is a setting in which every definable subset of the line is tame: a finite union of points and open intervals. This single axiom rules out oscillation, space-filling behavior, and other pathologies, and it makes one-variable definable functions tractable. The central consequence is the **Monotonicity Theorem**: every definable function on an interval is piecewise constant or strictly monotone and continuous, with only finitely many pieces.
The result originates in the work of Pillay and Steinhorn on o-minimality and is presented systematically in Lou van den Dries, *Tame Topology and O-minimal Structures*, Chapter 3 ([Cambridge University Press, 1998](https://doi.org/10.1017/CBO9780511529219)). A concise expository account is given in Mário Edmundo, *O-minimal structures* ([arXiv:math/0012051](https://arxiv.org/abs/math/0012051)). This mission formalizes the one-dimensional monotonicity theorem and its supporting lemmas in Lean 4 against Mathlib, as a verified entry point to o-minimal geometry.
## Setting
Let $R$ be a type equipped with a **dense linear order without endpoints** $D$: an irreflexive, transitive, trichotomous relation $D.\mathrm{lt}$ in which every strict inequality admits an interpolant and every element has strict predecessors and successors. Finite Cartesian powers are represented as coordinate tuples $\mathrm{Power}\,R\,n := \mathrm{Fin}\,n \to R$, with coordinate projections, deletion, and append operations defined explicitly.
An **o-minimal structure** $M$ over $D$ is a family $M.S\,n$ of collections of subsets of $\mathrm{Power}\,R\,n$, closed under finite unions and intersections, containing diagonals and the order relation, closed under products, coordinate reindexing, and existential projection, and satisfying the o-minimality axiom: every member of $M.S\,1$ is a finite union of points and open intervals. A **definable function** $f$ with domain $I$ and codomain $B$ is a dependent function on the corresponding subtypes whose domain, codomain, and graph are all members of $M$.
For $a < b$ in $\mathrm{Power}\,R\,1$, the **open interval** $(a,b)$ is the set of coordinate tuples whose single coordinate lies strictly between the two endpoint values, with endpoint variants allowing $-\infty$ and $+\infty$. A function is **strictly increasing** (respectively **strictly decreasing**) on $I$ when $x < y$ implies $f(x) < f(y)$ (respectively $f(y) < f(x)$) in the first output coordinate. **Continuity** at a domain point is the graph-based epsilon-delta predicate: $x$ belongs to $\mathrm{ContinuousPoints}\,D\,I\,G$ exactly when the graph $G$ meets every sufficiently small box around $(x, f(x))$ in the graph of a locally oscillation-free correspondence. Finiteness and infinitude of one-dimensional sets are expressed through first-coordinate listings.
## Formalization targets
### Goal — Monotonicity theorem
$$f : I \to B\ \text{definable},\ I\ \text{infinite} \implies \exists\, a = p_0 < p_1 < \cdots < p_k = b\ \text{with each}\ (p_i, p_{i+1})\ \text{good}.$$
An open cell $(p_i, p_{i+1})$ is **good** when $f$ restricted to $I \cap (p_i,p_{i+1})$ is constant, or strictly increasing and continuous there, or strictly decreasing and continuous there. The number $k$ of cut points is finite and depends on $f$, $a$, and $b$; no bound on $k$ is asserted.
### Supporting targets
$$I\ \text{definable and infinite} \implies I\ \text{contains a nonempty open interval}.$$
$$f\ \text{definable} \implies \text{each value fiber}\ f^{-1}(z)\ \text{is definable}.$$
$$\text{Either some value fiber is infinite or every value fiber is finite}.$$
$$f\ \text{definable on infinite}\ I \implies f\ \text{is constant or injective on some subinterval}.$$
$$f\ \text{injective and definable} \implies f\ \text{is strictly monotone on some subinterval}.$$
$$f\ \text{strictly monotone and definable} \implies f\ \text{is continuous on some subinterval}.$$
## Significance
*The result itself.* The Monotonicity Theorem is the foundation of one-dimensional o-minimal geometry. It implies that definable sets have finitely many connected components, that definable functions have finite limits at endpoints, and that higher-dimensional cell decomposition can proceed by induction on dimension. Without it, the correspondence between definability and geometric tameness remains unestablished.
*Formalizing it.* The classical proofs are known and appear in the references above; what is missing is a machine-checked version with explicit definability bookkeeping. This mission produces Lean 4 declarations for the order, interval, monotonicity, graph, and continuity predicates together with the theorem and its lemmas, all verified against the pinned Mathlib revision. The definability infrastructure (products, projections, fiber extraction) is reusable for subsequent cell-decomposition missions. Status honesty: the one-dimensional interval-extraction lemmas are machine-checked; the local constancy-or-injectivity lemma, the injective-to-monotone lemma, the finite-partition assembly, and the goal theorem itself remain open targets.
## Difficulty
The naive argument fixes a point and inspects nearby values, but definability does not by itself provide any neighborhood on which behavior is uniform. The fiber dichotomy illustrates the obstruction: knowing that each fiber $f^{-1}(z)$ is definable does not decide whether some fiber contains an interval or every fiber is finite, and the two cases require different constructions (a constancy interval versus an injective-selection interval). Similarly, injectivity alone does not yield monotonicity without partitioning the domain by local sign patterns and applying o-minimality to select a uniform pattern on a subinterval. Each step fails until the relevant definable set is exhibited and the one-dimensional interval lemma is applied to it.
## Formalization scope
Lean represents one-dimensional points as functions $\mathrm{Fin}\,1 \to R$, with order, intervals, and finiteness stated through the first coordinate. Definability is always the structure membership predicate $M.S\,n$, never an informal attribute. Continuity is the graph-based $\mathrm{ContinuousPoints}$ predicate applied to $\mathrm{FunctionGraph}\,f.\mathrm{toFun}$; a submission that discharges a continuity goal from the domain inclusion alone, or that replaces the continuity predicate by the domain set, does not satisfy the statement. The goal quantifies over cut points $p : \mathrm{Fin}\,(k+1) \to \mathrm{Power}\,R\,1$ with $p_0 = a$, $p_{\mathrm{last}} = b$, and strict increase at each step; the intervening sets $J$ are the open intervals determined by consecutive finite endpoints.
Contributions welcome: direct proofs of the open leaves (fiber definability, the finite-fiber injective-interval construction, the injective-to-monotone step, the finite-partition assembly), sharper statements with explicit endpoint bounds, and reusable o-minimal infrastructure beyond this mission. Out of scope: higher-dimensional cell decomposition, differentiability, and integration of definable functions.
## Selected references
- Lou van den Dries, Tame Topology and O-minimal Structures, London Mathematical Society Lecture Note Series 248, Cambridge University Press, 1998, Chapter 3. DOI: 10.1017/CBO9780511525919.
- Mário J. Edmundo, An Introduction to O-minimal Structures, 2000. arXiv:math/0012051.
Ngo's Fundamental Lemma I: Discriminant, Resultant and the Transfer FactorResearch Paper
## Motivation
The **fundamental lemma** is a family of identities between orbital integrals on a reductive
group and stable orbital integrals on a smaller group attached to it, its *endoscopic group*.
Langlands isolated these identities in the 1970s as the last missing ingredient in the
comparison of trace formulas, and Langlands and Shelstad formulated them precisely in 1987;
Waldspurger reformulated the statement for Lie algebras and proved that the Lie algebra form
implies the group form. The Lie algebra statement was proved in equal characteristic by
Bao Chau Ngo in *Le lemme fondamental pour les algebres de Lie*, Publ. Math. IHES **111**
(2010), 1-169 ([DOI](https://doi.org/10.1007/s10240-010-0026-7)), by a global geometric
argument built on the Hitchin fibration; Waldspurger's earlier work transfers the result to
mixed characteristic. The identity is the engine behind the stabilization of the trace
formula and behind the computation of the cohomology of Shimura varieties.
Both sides of the identity carry a normalizing factor built from the **discriminant**, and
the exact power of $q$ relating the two normalizations is fixed by a purely root-theoretic
computation carried out in Ngo's §1.10-§1.11. That computation is the subject of this
mission. It is self-contained, it uses no geometry, and it is the first piece of the paper
that can be stated in Lean today.
## Setting
Let $G$ be a split reductive group over a field with maximal torus $T$, character lattice
$X^*(T)$, cocharacter lattice $X_*(T)$, root system $\Phi \subset X^*(T)$ and Weyl group $W$.
Write $\mathfrak{t}$ for the Cartan subalgebra, so that each root $\alpha$ has a differential
$d\alpha$, a linear form on $\mathfrak{t}$. Ngô's **discriminant** is the product
$$ D_G \;=\; \prod_{\alpha \in \Phi} d\alpha , $$
a $W$-invariant polynomial function on $\mathfrak{t}$ and hence a function on the space
$\mathfrak{c} = \mathfrak{t} /\!/ W$ of characteristic polynomials.
An **endoscopic datum** is an element $\kappa$ of the dual torus
$\hat{T} = \operatorname{Hom}(X_*(T), \mathbb{G}_m)$. The endoscopic group $H$ attached to it
is the group whose root system is
$$ \Phi_H \;=\; \{\alpha \in \Phi \;:\; \kappa(\alpha^\vee) = 1\} , $$
with Weyl group $W_H \subset W$ and its own discriminant $D_H = \prod_{\alpha \in \Phi_H}
d\alpha$. Choose a subset $\Lambda \subset \Phi - \Phi_H$ containing exactly one root out of
each pair $\{\alpha, -\alpha\}$ of opposite roots outside $\Phi_H$, and set
$$ R^G_H \;=\; \prod_{\alpha \in \Lambda} d\alpha . $$
Finally let $F$ be a non-archimedean local field with valuation $v$ and residue cardinality
$q$, and recall Ngô's normalizing factors $\Delta_G(a) = q^{-v(D_G(a))/2}$ and
$\Delta_H(a_H) = q^{-v(D_H(a_H))/2}$.
## Formalization targets
### Goal (1.11.3): the transfer factor identity
$$ v\bigl(D_G(a)\bigr) \;=\; v\bigl(D_H(a_H)\bigr) \;+\; 2\, v\bigl(R^G_H(a_H)\bigr) $$
for a point $a_H$ of the endoscopic Cartan with image $a$. Equivalently
$\Delta_H(a_H)\Delta_G(a)^{-1} = q^{\,r}$ with $r = v(R^G_H(a_H))$: this is exactly what lets
one pass between the two forms of the fundamental lemma,
$O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}) = q^{\,r} SO_{a_H}(\mathbf{1}_{\mathfrak{h}})$ and
$\Delta_G(a) O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}) = \Delta_H(a_H)
SO_{a_H}(\mathbf{1}_{\mathfrak{h}})$.
### Milestones
The identity above is the image under $v$ of the divisor identity $\nu^* D_G = D_H + 2 R^G_H$
of 1.10.3, which in turn rests on the fact that $R^G_H$ — which depends on a choice of
$\Lambda$ — is nevertheless $W_H$-invariant, and on the fact that $\Phi_H$ really is a root
subsystem. The milestone list follows that order.
## Significance
Theorem 1 of Ngô's paper, the Langlands-Shelstad conjecture for Lie algebras, is the identity
$\Delta_G(a) O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}, dt) = \Delta_H(a_H)
SO_{a_H}(\mathbf{1}_{\mathfrak{h}}, dt)$ for corresponding regular semisimple stable classes,
under the hypothesis that twice the Coxeter number of $G$ is smaller than the residue
characteristic. Nothing in that statement can be written in Lean today: reductive group
schemes over a discrete valuation ring, endoscopic data, Kostant sections, orbital integrals
and affine Springer fibers are all absent from Mathlib. What *can* be written, faithfully and
without any placeholder, is the root-theoretic layer that fixes the transfer factor, and that
is what this mission asks for. It is a genuine prerequisite: the two displayed forms of
Theorem 1 differ precisely by the identity above.
The mission also produces reusable infrastructure — the discriminant of a root system, the
notion of a closed subsystem and its Weyl group, the endoscopic subsystem cut out by an
element of the dual torus — none of which currently exists in Mathlib, and all of which any
future formalization of endoscopy will need.
## Difficulty
Only one of the four milestones is a routine manipulation. Splitting
$\Phi - \Phi_H$ into pairs $\{\alpha,-\alpha\}$ and collecting squares is bookkeeping; that
$D_G$ is $W$-invariant is immediate because $W$ permutes $\Phi$. The content is in Lemma
1.10.2: $\Lambda$ is *not* stable under $W_H$, so $w \in W_H$ carries
$\prod_{\alpha\in\Lambda} d\alpha$ to $(-1)^{m(w)} \prod_{\alpha\in\Lambda} d\alpha$, where
$m(w)$ counts the roots of $\Lambda$ sent into $-\Lambda$; the claim is that $m(w)$ is always
even. The naive attempt — check it on the generating reflections of $W_H$ — is exactly where
a careless argument goes wrong, since it is false for reflections in roots outside $\Phi_H$.
Ngô's argument identifies the sign with $(-1)^{\ell_G(w)} (-1)^{\ell_H(w)}$, the ratio of the
sign characters of $W$ and $W_H$, and observes that both compute the determinant of $w$ acting
on the same reflection representation.
## Formalization scope
Root systems are modelled with Mathlib's `RootPairing ι R M N`: the module $M$ plays the role
of $X^*(T)$, the module $N$ the role of $X_*(T)$ and of the Cartan on which the differentials
$d\alpha$ are evaluated, and $P.root' i$ is the linear form $d\alpha$. The endoscopic
subsystem is cut out by an element $\kappa$ of the dual torus, taken as a group homomorphism
from the cocharacter lattice to an arbitrary commutative group, and is expressed over $\mathbb{Z}$
coefficients as in the definition of a root datum. Products over $\Phi$ and $\Phi_H$ are
finite products over a `Fintype` index, and a choice $\Lambda$ is a `Finset` satisfying an
exclusive-or condition, which automatically rules out the degenerate case $\alpha = -\alpha$.
The identity 1.10.3 is stated as an identity of functions on the Cartan rather than as an
identity of divisors, so the unit $(-1)^{|\Lambda|}$ is carried explicitly rather than
discarded. Lemma 1.10.2 is stated over $\mathbb{Q}$ for an honest root system, since the
sign argument uses the reflection representation. The goal 1.11.3 is stated for an additive
valuation with values in $\mathbb{Z} \cup \{\infty\}$, which is what makes the two sides
comparable when a discriminant vanishes.
There is no trivializing formalization here: the hypotheses of every item are satisfiable —
any root system with any closed subsystem and any choice of $\Lambda$ gives an instance — so
none of the statements is vacuous, and none of them is an identity between two occurrences of
the same expression.
Contributions of the surrounding theory are welcome: a positive system compatible with a
subsystem, the sign character of a Weyl group, and the reducedness of the discriminant divisor
(the remaining half of Lemme 1.10.1) are all natural next steps.
## Selected references
- Bao Chau Ngo, *Le lemme fondamental pour les algebres de Lie*, Publ. Math. IHES 111 (2010), 1-169. https://doi.org/10.1007/s10240-010-0026-7
- R. Langlands, D. Shelstad, *On the definition of transfer factors*, Math. Ann. 278 (1987), 219-271. https://doi.org/10.1007/BF01458070
- J.-L. Waldspurger, *Endoscopie et changement de caracteristique*, J. Inst. Math. Jussieu 5 (2006), 423-525. https://doi.org/10.1017/S1474748006000041
- R. Kottwitz, *Transfer factors for Lie algebras*, Represent. Theory 3 (1999), 127-138. https://doi.org/10.1090/S1088-4165-99-00077-6
- T. Hales, *A statement of the fundamental lemma*, in Harmonic Analysis, the Trace Formula, and Shimura Varieties, Clay Math. Proc. 4 (2005), 643-658. https://arxiv.org/abs/math/0312227
An Introduction to Chaotic Dynamical Systems II: Sarkovskii's TheoremTextbook
## Motivation
In 1964 A. N. Sarkovskii proved a theorem about continuous maps of the real line that is
remarkable both for how little it assumes — continuity, nothing more — and for how much it
concludes: the set of periods of the periodic orbits of such a map is completely constrained
by a single linear ordering of the positive integers. Its best-known corollary, rediscovered
by Li and Yorke in 1975 under the slogan *period three implies chaos*, says that a continuous
map of $\mathbb{R}$ with an orbit of period three has orbits of every period.
Devaney presents the theorem in §1.10 of *An Introduction to Chaotic Dynamical Systems* (2nd
edition, Westview Press, 2003), calling it the chapter's first major theorem, and gives the
elementary proof of Block, Guckenheimer, Misiurewicz and Young based on interval covering
relations. This mission is the second in a series formalizing the book; it is independent of
the first, sharing only the book-wide namespace.
Timeline: Sarkovskii (1964) proved the full ordering theorem, in Ukrainian, and it went largely
unnoticed in the West; Li and Yorke (1975) independently proved the period-three case and gave
the field the word "chaos"; Štefan (1977) and Block–Guckenheimer–Misiurewicz–Young (1980) gave
the short interval-covering proofs, the latter being the one Devaney reproduces.
## Setting
Let $f : \mathbb{R} \to \mathbb{R}$ be continuous. A point $x$ has **prime period** $n \ge 1$
if $f^{n}(x) = x$ and $f^{m}(x) \ne x$ for every $0 < m < n$.
The **Sarkovskii ordering** of the positive integers is
$$3 \,\triangleright\, 5 \,\triangleright\, 7 \,\triangleright\, \cdots \,\triangleright\,
2\cdot 3 \,\triangleright\, 2\cdot 5 \,\triangleright\, \cdots \,\triangleright\,
2^2\cdot 3 \,\triangleright\, 2^2 \cdot 5 \,\triangleright\, \cdots \,\triangleright\,
2^3 \,\triangleright\, 2^2 \,\triangleright\, 2 \,\triangleright\, 1 :$$
first the odd numbers greater than one in increasing order, then $2$ times the odds, then
$2^2$ times the odds, and so on; the powers of two come last, in decreasing order. Writing
$k = 2^{a}p$ and $\ell = 2^{b}q$ with $p, q$ odd, $k \triangleright \ell$ holds exactly when
either $p, q > 1$ and $(a,p)$ precedes $(b,q)$ lexicographically, or $p > 1$ and $q = 1$, or
$p = q = 1$ and $b < a$.
Two elementary facts drive the proof. If $I$ is a closed interval with $f(I) \supseteq I$,
then $f$ has a fixed point in $I$; and if closed intervals satisfy
$f(A_i) \supseteq A_{i+1}$ for $i < n$, then some point of $A_0$ has $f^{i}(x) \in A_i$ for all
$i \le n$. One writes $I \to J$, "$f(I)$ covers $J$", for $J \subseteq f(I)$.
## Target
The goal is Devaney's Theorem 10.2: for continuous $f : \mathbb{R} \to \mathbb{R}$,
$$\text{if } f \text{ has a point of prime period } k \text{ and } k \triangleright \ell,
\text{ then } f \text{ has a point of prime period } \ell .$$
The milestones are the steps of the book's proof: the two covering observations, the
period-three special case (Theorem 10.1), the odd case, the power-of-two case and the mixed
case $p \cdot 2^m$ into which the general theorem is decomposed, the remark that a period which
is not a power of two forces infinitely many periodic points, and the converse direction,
witnessed by the piecewise-linear map with a period-five orbit and no period-three orbit.
## Significance
Sarkovskii's theorem is the sharpest general statement known about the period structure of
one-dimensional dynamics, and it is sharp in both directions: the ordering is realized, so no
stronger implication holds. Its first consequence — only powers of two can occur as the set of
periods of a map with finitely many periodic points — is what makes the period-doubling
cascade the canonical route to chaos, a theme the book returns to in §1.17.
The theorem is emphatically one-dimensional: it fails on the circle, where a rotation by
$120^\circ$ has every point of period three and no other period.
Formalizing it contributes a reusable Lean treatment of interval covering relations and of the
Sarkovskii ordering itself; we are not aware of these in Mathlib at the pinned revision, and
the covering machinery is exactly what §1.13 and §1.16 of the book reuse.
## Difficulty
The period-three case is a short argument once the covering observations are available, and it
is a reasonable first milestone. The general theorem is not: the odd case requires choosing the
right interval $I_1 = [x_i, x_{i+1}]$ on the orbit, building the increasing family of unions
$O_\ell$ of covered intervals, and showing that the shortest return loop has length exactly
$n-1$ — a combinatorial argument on the cyclic order of the orbit that is easy to draw and
tedious to formalize. Attempts to shortcut the ordering with a naive induction on $n$ fail:
the statement for $n$ genuinely depends on the geometric arrangement of the orbit points.
## Formalization scope
1. Periodicity is *prime* period throughout: $f^n(x) = x$ together with minimality of $n$. The
statements would be false or trivial with "period" read as "fixed by $f^n$".
2. The Sarkovskii relation is defined arithmetically, in terms of the $2$-adic valuation and
the odd part of an integer, rather than as a listed order; it is a strict relation, so
$k \triangleright k$ is false and the goal theorem says nothing about $\ell = k$ (which
holds by hypothesis anyway).
3. $0$ is outside the ordering: the relation is false whenever either argument is $0$.
4. Intervals in the covering lemmas are closed intervals $[a,b]$ with $a \le b$, given by their
endpoints; "covers" means containment of the interval in the *image*, $J \subseteq f(I)$.
5. The converse milestone asserts the existence of a continuous map with a period-five point
and no period-three point; the book's witness is piecewise linear on $[1,5]$, but the
statement does not prescribe it.
## Selected references
- Robert L. Devaney, *An Introduction to Chaotic Dynamical Systems*, 2nd edition, Westview
Press, 2003 (ISBN 0-8133-4085-3) — §1.10, pp. 60–68. The mission's primary source.
- T. Y. Li and J. A. Yorke, *Period three implies chaos*, American Mathematical Monthly 82
(1975), 985–992, DOI:
[10.1080/00029890.1975.11994008](https://doi.org/10.1080/00029890.1975.11994008).
- L. Block, J. Guckenheimer, M. Misiurewicz, L. S. Young, *Periodic points and topological
entropy of one-dimensional maps*, in Global Theory of Dynamical Systems, Lecture Notes in
Mathematics 819, Springer, 1980, 18–34, DOI:
[10.1007/BFb0086977](https://doi.org/10.1007/BFb0086977) — the proof Devaney follows.
## Audit note (provenance of the read-backs)
**The read-backs attached to every draft item in this proposal are not independent.** They were
written by the same agent that drafted the Lean statements, not by a separate auditor working
blind from the code alone. They are included because they are still useful as a line-by-line
rendering of each statement, but they are **not** independent testimony: any misreading baked
into a formalization is likely repeated in its read-back, and agreement between the two should
not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own
first paragraph. Reviewers who want independent testimony should commission fresh, blind
read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`): all files
elaborate with no errors, the only warnings being the expected `sorry` placeholders in the
theorem bodies.
Herzog-Schönheim for subnormal coversResearch Paper
## Motivation
A **coset partition** of a group $G$ is a finite family of left cosets $a_1G_1, \dots, a_kG_k$
that are pairwise disjoint and cover $G$. In 1974 [Herzog and
Schönheim](https://doi.org/10.4153/CMB-1974-025-7) asked whether the indices
$n_i = [G : G_i]$ of such a partition, with $k > 1$, can be pairwise distinct. They cannot when
$G = \mathbb{Z}$ — there a coset partition is an *exact covering system* of the integers, and
Davenport–Rado and Mirsky–Newman showed the largest modulus must repeat — but for general groups
the question is still open, even for finite solvable groups.
Progress has come in two styles. *Structural*: Berger, Felzenbaum and Fraenkel settled finite
**nilpotent** groups in [Canad. Math. Bull. 29 (1986)
329–333](https://doi.org/10.4153/CMB-1986-050-0) and finite **pyramidal** groups in [Fund. Math.
128 (1987) 139–144](https://doi.org/10.4064/fm-128-3-139-144). *Order-bounded*: [Ginosar and
Schnabel (2011)](https://www.researchgate.net/publication/265126234) settled every $G$ whose
order has at most two prime divisors, and [Margolis and Schnabel
(2019)](https://arxiv.org/abs/1803.03569) verified all $|G| < 1440$.
The paper formalized here, [Z.-W. Sun, *J. Algebra* **273** (2004)
153–175](https://doi.org/10.1016/S0021-8693(03)00526-X), takes a third route: it constrains the
*subgroups* rather than the group, and simultaneously weakens "partition" to "uniform cover".
Its hypothesis — that the $G_i$ be **subnormal** — costs nothing in the nilpotent case (every
subgroup of a nilpotent group is subnormal) yet applies to arbitrary, possibly infinite, ambient
groups $G$. It also answers negatively an open question of the same paper, generalizing one of
Erdős: the indices of such a cover cannot all be large if each occurs only boundedly often.
## Setting
Let $G$ be a group, written multiplicatively. For a finite system
$$ \mathcal{A} = \{a_iG_i\}_{i=1}^{k} $$
of left cosets, the **covering function** counts memberships,
$$ w_{\mathcal{A}}(x) \;=\; \bigl|\{\, 1 \le i \le k \;:\; x \in a_iG_i \,\}\bigr| . $$
If $w_{\mathcal{A}}$ is constant, say $w_{\mathcal{A}} \equiv w$, then $\mathcal{A}$ is a
**uniform cover** of $G$ of weight $w$; the case $w = 1$ is exactly a coset partition. A uniform
cover is **trivial** when $G_i = G$ for every $i$, and this is the only degenerate case that must
be excluded. Uniform covers are genuinely more general than partitions: one may have no disjoint
subcover at all.
A subgroup $H \le G$ is **subnormal** if some finite chain
$H = H_0 \trianglelefteq H_1 \trianglelefteq \cdots \trianglelefteq H_n = G$ reaches $G$, each
term normal in the next. Normal subgroups are subnormal; in a nilpotent group every subgroup is;
and $\operatorname{Sym}(4)$ shows a subgroup of a solvable group need not be.
Write $n_i = [G : G_i]$ for the indices, always assumed finite, and
$$ N \;=\; [\,n_1, \dots, n_k\,] $$
for their least common multiple, whose prime divisors are exactly those of $n_1\cdots n_k$. Let
$p_*$ and $p^*$ denote the least and greatest prime divisors of $N$, let $\varphi$ be Euler's
totient, and let
$$ M \;=\; \max_{1 \le j \le k} \bigl|\{\, 1 \le i \le k : n_i = n_j \,\}\bigr| $$
be the largest multiplicity with which an index is repeated. The Herzog–Schönheim conjecture says
$M \ge 2$.
## Target
The goal theorem is Theorem 4.3(i) of the source: for a nontrivial uniform cover of any group by
cosets of subnormal subgroups of finite index, some index divisible by the largest prime $p^*$ is
repeated at least $p_*$ times,
$$ \exists\, j, \qquad p^* \mid n_j \quad\text{and}\quad
\bigl|\{\, i : n_i = n_j \,\}\bigr| \;\ge\; p_* . $$
In particular $M \ge p_*$. Two weaker consequences are separate targets. Since $p_* \ge 2$, this
gives the **Herzog–Schönheim conjecture for subnormal uniform covers**,
$$ \exists\, i \ne j, \qquad [G : G_i] = [G : G_j], $$
and the quantitative step behind it is a **Burshtein-type inequality**, which after clearing
denominators reads
$$ p^{*}\prod_{p \mid N}(p-1) \;<\; \bigl|\{\, i : n_i = n_j \,\}\bigr| \prod_{p \mid N} p
\qquad\text{for some } j \text{ with } p^* \mid n_j . $$
## Significance
*The result itself.* It is the widest structural class in which Herzog–Schönheim is known, and
the only one that does not require $G$ to be finite: subnormality of the $G_i$ is a condition on
the *subgroups*, so $G$ itself is arbitrary. It strictly contains the nilpotent case of
Berger–Felzenbaum–Fraenkel, and being quantitative it also yields the Burshtein conjecture in
this setting — a bound no purely qualitative statement gives. Because the conclusion is a lower
bound on $M$ growing with $p_*$, it answers the paper's open question: one cannot make all the
indices of a uniform cover large while keeping every multiplicity bounded.
*Formalizing it.* Nothing here is open, and the mission is the machine-checked version of a known
proof. What it adds is a formal vocabulary for *uniform* covers — Mathlib has
`Mathlib/GroupTheory/CosetCover.lean` (B. H. Neumann's theorems, $\sum_i 1/[G:H_i] \ge 1$) but no
notion of covering multiplicity — and the arithmetic of subnormality, in particular that
$[G : \bigcap_i G_i]$ *divides* $\prod_i [G : G_i]$ when the $G_i$ are subnormal. Mathlib has
`Subgroup.IsSubnormal` with the basic closure properties but nothing about indices of subnormal
subgroups, and that divisibility is the whole reason subnormal covers behave. The totient measure
this proof runs on is already formalized: Sun's Lemma 3.1 is Berger–Felzenbaum–Fraenkel's equation
(14), already proved on the platform as `BFFPyramidal.muMeasure_divisorClosure_image_mul`, and
this mission reuses that definition file rather than duplicating it.
**Status disclosure.** Complete Lean proofs of the goal and of every milestone below already
exist and will be submitted at launch, so this mission is not an open frontier: its value is the
verified artifact, the reusable vocabulary, and the fact that the development turned up two
places where the published argument needs repair or can be simplified (see *Formalization
scope*). Alternative proofs, sharper variants, and the analytic parts excluded below remain
genuinely open contributions.
## Difficulty
The reciprocal identity is the first thing anyone writes down and it is not enough: a uniform
cover of weight $w$ satisfies $\sum_i 1/n_i = w$, and pairwise distinct $n_i$ can do that.
The real obstruction is that **a cover does not descend to a quotient**. A part $a_iG_i$ need not
lie in one coset of a chosen normal subgroup, so the induction that proves the finite nilpotent
case has nothing to induct along once $G$ may be infinite and the $G_i$ are merely subnormal.
Sun's replacement is a lower bound for the *size of a union of cosets*, Theorem 3.1: if
$H \le G_i$ for all $i$ and $[G:H] < \infty$, then the number of cosets of $H$ inside
$\bigcup_i a_iG_i$ is at least the number of $n < [G:H]$ divisible by some $n_i$. The union is
compared not with the $G_i$ but with a purely numerical shadow of itself in
$\{0, 1, \dots, [G:H]-1\}$, and it is here that subnormality enters, through the divisibility
$[G : \bigcap G_i] \mid \prod [G : G_i]$ (Lemma 2.1) — for arbitrary finite-index subgroups
Poincaré gives only the inequality $[G : \bigcap G_i] \le \prod [G:G_i]$, which is too weak.
The second difficulty is arithmetic and is where the source spends its effort. Turning
Theorem 3.1 into a bound on multiplicities (Theorem 3.2) requires computing the density of a
union $\bigcup_i n_i\mathbb{Z}$, and the identity the paper uses (Lemma 3.4) expresses that
density as $\prod_{p \in P}\frac{p-1}{p}$ times an **infinite** sum of reciprocals over
$P$-smooth elements of the union. Along that route the full series is needed: truncating it loses
precisely the geometric factors $\bigl(1 - p^{-(1+\delta_p)}\bigr)^{-1}$ that produce the divisor
sum $\sum_{d \mid N/g} 1/d$ in the conclusion.
It is worth saying, though, that this analytic detour is **avoidable** — a solver need not take
it. Theorem 3.2 can also be reached by a purely finite argument: bound the density from below by
injecting each index $s$ into the divisor $\operatorname{lcm}\{s' : s' \mid x\}/s$, which is
sharp in the same cases as the series argument. Lemma 3.4 remains a faithful and separately
interesting milestone of the paper, but it is not on the critical path to the goal. The naive
version of the finite estimate — bounding the density below by $1/\min_i n_i$ — is genuinely
false, as $\{4,6,9,12,18,36\}$ shows, so the injection is the content, not a one-liner.
## Formalization scope
The development commits to the following conventions, worth stating because the prose leaves them
implicit.
Covers are indexed families rather than sets of cosets: `IsUniformCover K a w` asserts that for
every $x$ the number of indices $i$ with $(a_i)^{-1}x \in K_i$ is exactly `w`, counted as
`Nat.card` of a subtype so that no decidability hypothesis is needed. Indexing by `Fin k` keeps
multiplicities visible, which matters because every conclusion counts indices, not distinct
subgroups. Nontriviality is *never* folded into the definition; it appears as the explicit
hypothesis `∃ i, K i ≠ ⊤`, and without it every statement here is false (take $k=1$, $G_1 = G$).
$G$ is an arbitrary group — **not** assumed finite. Finiteness enters only through
`Subgroup.FiniteIndex` on each $K_i$, which the source assumes implicitly when it writes "the
(finite) indices". Indices are `Subgroup.index` and $[G_i : H]$ is `H.relIndex (K i)`. For a
subgroup $H$ that is *not* assumed normal, `G ⧸ H` is still the type of left cosets and
`Nat.card (G ⧸ H) = H.index`; Theorem 3.1 is stated with that type, since the $H$ it is applied
to is not normal.
Densities are never limits. The density of a union $\bigcup_i n_i\mathbb{Z}$ is taken as the
finite ratio $|\{x < N : \exists i,\ n_i \mid x\}| / N$ for an explicit common multiple $N$,
which is exactly equal to the asymptotic density and keeps Lemma 3.4 free of any analysis on the
left-hand side; the right-hand side genuinely is an infinite sum and is stated with `HasSum` over
$\mathbb{R}$.
Inequalities are cleared of denominators and stated in $\mathbb{N}$ wherever possible, so that
$\sum_{d \mid m} 1/d \le c$ appears as $\sum_{d \in m.divisors} d \le c \cdot m$. Readers should
check the direction: $\mathbb{N}$ subtraction truncates, so $\prod_{p \mid N}(p-1)$ is only the
intended quantity because every $p$ here is prime, hence $\ge 2$.
⚠️ **Parts (ii)–(iv) of the source's Theorem 4.3 are out of scope.** Those bound the primes
dividing the indices, their number, and $\log n_1$ by $e^{\gamma}M\log^2 M + O(M \log M \log\log
M)$ and similar, and they rest on **Mertens' third theorem**,
$\prod_{p \le x}(1 - 1/p) \sim e^{-\gamma}/\log x$, which Mathlib does not have. It is worth
being precise about what Mathlib *does* have, since the gap is narrower than it looks: the prime
counting function `Nat.primeCounting`, Chebyshev's $\theta$ and $\psi$ with the machinery around
them (`Mathlib/NumberTheory/Chebyshev.lean`), Euler products
(`Mathlib/NumberTheory/EulerProduct/`), and the constant $\gamma$ itself
(`Real.eulerMascheroniConstant`) are all present — what is missing is Mertens' asymptotic tying
them together, and the $\pi(x)$ asymptotics. Supplying that is a substantial number-theory
project in its own right, so this mission stops at the arithmetic core, part (i), which is what
implies Herzog–Schönheim. Contributions adding the analytic parts are welcome and would complete
Theorem 4.3.
Two things the development established that the paper does not state. First, Lemma 2.1 is true
in a **stronger** form: $[G : A \cap B] \mid [G:A]\,[G:B]$ needs only $A$ subnormal, not both, and
needs no finiteness hypothesis at all (with Mathlib's convention that an infinite index is $0$).
Second, Theorem 4.1's passage from the largest prime $p^*$ to the smallest $p_*$ can be isolated
as a self-contained arithmetic inequality, $(p_*-1)\prod_{p\mid N}p \le p^*\prod_{p\mid N}(p-1)$,
which is tight at prime powers; it is listed as its own milestone for that reason.
Reusable beyond this mission: the uniform-cover vocabulary, the subnormal index divisibility of
Lemma 2.1, and Theorem 3.1's union bound, which applies to any attack on Herzog–Schönheim
including the still-open solvable case. The source also leaves **Conjecture 4.1** open — that for
a nontrivial uniform cover by subnormal subgroups the *largest* index $n$ is repeated at least
$p(n)$ times, $p(n)$ its least prime factor — which would be a natural follow-on target.
## Selected references
- Z.-W. Sun, *On the Herzog–Schönheim conjecture for uniform covers of groups*, Journal of Algebra **273** (2004) 153–175. [DOI](https://doi.org/10.1016/S0021-8693(03)00526-X)
- M. Herzog, J. Schönheim, *Research problem No. 9*, Canadian Mathematical Bulletin **17** (1974) 150.
- M. A. Berger, A. Felzenbaum, A. S. Fraenkel, *The Herzog–Schönheim conjecture for finite nilpotent groups*, Canadian Mathematical Bulletin **29** (1986) 329–333. [DOI](https://doi.org/10.4153/CMB-1986-050-0)
- M. A. Berger, A. Felzenbaum, A. S. Fraenkel, *Remark on the multiplicity of a partition of a group into cosets*, Fundamenta Mathematicae **128** (1987) 139–144. [DOI](https://doi.org/10.4064/fm-128-3-139-144)
- N. Burshtein, *On natural exactly covering systems of congruences having moduli occurring at most M times*, Discrete Mathematics **14** (1976) 205–214. [DOI](https://doi.org/10.1016/0012-365X(76)90033-0)
- R. J. Simpson, *Exact coverings of the integers by arithmetic progressions*, Discrete Mathematics **59** (1986) 181–190. [DOI](https://doi.org/10.1016/0012-365X(86)90372-2)
- Z.-W. Sun, *Exact m-covers of groups by cosets*, European Journal of Combinatorics **22** (2001) 415–429. [DOI](https://doi.org/10.1006/eujc.2000.0413)
- B. H. Neumann, *Groups covered by finitely many cosets*, Publicationes Mathematicae Debrecen **3** (1954) 227–242.
- L. Margolis, O. Schnabel, *The Herzog–Schönheim conjecture for small groups and harmonic subgroups*, Beiträge zur Algebra und Geometrie **60** (2019) 399–418. [arXiv](https://arxiv.org/abs/1803.03569)
An Introduction to Chaotic Dynamical Systems I: Chaos in the Quadratic FamilyTextbook
## Motivation
The word *chaos* entered mathematics with a precise meaning, and Robert L. Devaney's
*An Introduction to Chaotic Dynamical Systems* (2nd edition, Westview Press, 2003) is the
text that fixed the meaning now used in most of the literature: a map is chaotic when it is
unpredictable (sensitive dependence on initial conditions), indecomposable (topological
transitivity), and nevertheless regular (dense periodic points). The book develops this
definition on the simplest possible object — the real quadratic family
$F_\mu(x) = \mu x(1-x)$ on the unit interval — and shows that for large $\mu$ the map is
chaotic on an invariant Cantor set, by exhibiting an exact symbolic model for it.
This mission is the first of a planned series formalizing the book. It covers §1.5–§1.8:
the invariant set of the quadratic family, symbolic dynamics on the sequence space
$\Sigma_2$, topological conjugacy, and Devaney's definition of chaos. Everything later in
the book — Sarkovskii's theorem, the horseshoe, hyperbolic toral automorphisms, Julia sets —
is written in the vocabulary fixed here, so a faithful Lean version of this chapter fixes the
vocabulary of the whole series.
## Setting
Write $I = [0,1]$ and let $F_\mu(x) = \mu x(1-x)$ for a real parameter $\mu$. Iterates are
written $F_\mu^n$, with $F_\mu^0$ the identity.
For $\mu > 4$ the maximum value $\mu/4$ of $F_\mu$ exceeds $1$, so some points of $I$ leave
$I$ after one iteration. Let
$$A_0 = \{x \in I : F_\mu(x) > 1\}, \qquad A_n = \{x \in I : F_\mu^{\,n}(x) \in A_0\},$$
so that $A_n$ is the set of points escaping from $I$ at the $(n+1)$-st iteration. The set of
points that never escape is
$$\Lambda = I \setminus \bigcup_{n \ge 0} A_n = \{x : F_\mu^{\,n}(x) \in I \text{ for all } n \ge 0\}.$$
The complement $I \setminus A_0$ consists of two closed intervals, $I_0$ to the left of the
midpoint $1/2$ and $I_1$ to its right.
On the symbolic side, $\Sigma_2$ is the set of one-sided infinite sequences
$s = (s_0 s_1 s_2 \dots)$ with $s_i \in \{0,1\}$, metrized by
$$d[s,t] = \sum_{i=0}^{\infty} \frac{|s_i - t_i|}{2^i},$$
and $\sigma : \Sigma_2 \to \Sigma_2$ is the shift map $\sigma(s_0 s_1 s_2 \dots) = (s_1 s_2 s_3 \dots)$.
The *itinerary* of $x \in \Lambda$ is the sequence $S(x) = (s_0 s_1 s_2 \dots)$ with $s_j = 0$
when $F_\mu^{\,j}(x) \in I_0$ and $s_j = 1$ when $F_\mu^{\,j}(x) \in I_1$.
Following Devaney, $f : J \to J$ is **topologically transitive** if for every pair of open
sets $U, V$ meeting $J$ there is $k > 0$ with $f^k(U \cap J) \cap V \neq \emptyset$; it has
**sensitive dependence on initial conditions** if there is $\delta > 0$ such that every point
of $J$ has points of $J$ arbitrarily near it whose orbit eventually separates from its own by
more than $\delta$; and it is **chaotic on $J$** when it has sensitive dependence, is
topologically transitive, and has a dense set of periodic points in $J$.
## Target
The goal is Devaney's Example 8.8: for $\mu > 2 + \sqrt 5$,
$$F_\mu \text{ is chaotic on } \Lambda .$$
The milestones are the results the book uses to get there, in the book's own order:
the escape of orbits outside $I$ (Proposition 5.2), the tame regime $1 < \mu < 3$
(Proposition 5.3), the Cantor structure of $\Lambda$ (Theorem 5.6), the metric and dynamics of
the shift (Propositions 6.3, 6.5, 6.6), the itinerary conjugacy (Theorems 7.2, 7.3), its
dynamical consequences (Theorem 7.5), sensitive dependence (Example 8.3), and the chaos of
$F_4$ on all of $I$ (Example 8.9).
## Significance
The theorem is the prototype for every later "chaos via symbolic dynamics" argument: the
horseshoe, hyperbolic toral automorphisms, and the quadratic Julia sets are all proved chaotic
by producing a conjugacy with a shift. The conjugacy also gives quantitative information that
is otherwise inaccessible — for example, that $F_\mu$ has exactly $2^n$ points fixed by
$F_\mu^{\,n}$, which no direct computation with the degree-$2^n$ polynomial delivers.
Formalizing it produces reusable Lean infrastructure that Mathlib currently lacks: Devaney's
three chaos conditions, the sequence space $\Sigma_2$ with its metric and shift, topological
conjugacy of maps on subsets, and the notion of a Cantor subset of the interval. These are the
foundation the rest of the book's series will import.
## Difficulty
The obvious route to the goal — analyze $F_\mu$ on $\Lambda$ directly — fails, because
$\Lambda$ has no explicit description: it is a nested intersection of $2^{n+1}$ intervals
whose endpoints are not available in closed form. The whole argument therefore goes through
the itinerary map, and its two hard steps are: (i) surjectivity of the itinerary map, which
needs the nested-interval construction $I_{s_0 \dots s_n} = I_{s_0} \cap F_\mu^{-1}(I_{s_1}) \cap
\dots \cap F_\mu^{-n}(I_{s_n})$ together with the fact that these intervals are nonempty and
nested; and (ii) injectivity, which needs the hyperbolicity estimate $|F_\mu'| > \lambda > 1$
on $I_0 \cup I_1$, valid exactly because $\mu > 2 + \sqrt 5$, and the mean value theorem. The
hypothesis $\mu > 2 + \sqrt 5$ is not cosmetic: Devaney notes the results hold for $\mu > 4$,
but only with a more delicate argument.
## Formalization scope
The Lean development fixes the following conventions.
1. $\Lambda$ is defined as $\{x : \forall n,\ F_\mu^{\,n}(x) \in [0,1]\}$ — the points whose
whole forward orbit stays in $I$ — rather than as a complement of the sets $A_n$; the two
descriptions agree, and the definitional form makes invariance immediate. The sets
$A_0, A_n, I_0, I_1$ are nonetheless defined, since the book's arguments refer to them.
2. The itinerary is defined as a total function of a real argument, taking entry $0$ at step
$n$ when $F_\mu^{\,n}(x) \le 1/2$ and $1$ otherwise. On $\Lambda$ this agrees with Devaney's
$I_0/I_1$ test, since the midpoint $1/2$ lies in the gap $A_0$ when $\mu > 4$.
3. $\Sigma_2$ carries Devaney's metric $d$ literally, as a summable series, not merely a
topology; the metric space instance is part of the definitional layer, so Proposition 6.2
is not a separate milestone.
4. Sensitive dependence, transitivity, chaos and periodicity are stated for a map
$f : X \to X$ of a metric space together with an invariant subset $J$, using open sets of
the ambient space intersected with $J$; this avoids subtype bookkeeping while keeping the
relative formulation of the book.
5. Cardinality claims ("$\operatorname{Per}_n$ has $2^n$ elements") are stated with
`Set.ncard` and are restricted to $n > 0$; for $n = 0$ every point is fixed by $F^0$ and the
claim would be false.
6. Nothing here is vacuous: the hypothesis $\mu > 2+\sqrt 5$ is satisfiable, $\Lambda$ is
nonempty (it contains $0$), and the chaos predicate is a conjunction of three nontrivial
conditions rather than a definitional abbreviation.
Contributions of any kind are welcome: full proofs, reductions splitting a milestone into
lemmas, and reusable lemmas about $\Sigma_2$ or about conjugacy that later missions in the
series can import.
## Selected references
- Robert L. Devaney, *An Introduction to Chaotic Dynamical Systems*, 2nd edition, Westview
Press, 2003 (ISBN 0-8133-4085-3) — §1.5 (pp. 31–38), §1.6 (pp. 39–43), §1.7 (pp. 44–47),
§1.8 (pp. 49–52). The mission's primary and authoritative source.
- J. Banks, J. Brooks, G. Cairns, G. Davis, P. Stacey, *On Devaney's definition of chaos*,
American Mathematical Monthly 99 (1992), 332–334, DOI:
[10.1080/00029890.1992.11995856](https://doi.org/10.1080/00029890.1992.11995856) — proves
that transitivity plus dense periodic points already imply sensitive dependence.
## Audit note (provenance of the read-backs)
**The read-backs attached to every draft item in this proposal are not independent.** They were
written by the same agent that drafted the Lean statements, not by a separate auditor working
blind from the code alone. They are included because they are still useful as a line-by-line
rendering of each statement, but they are **not** independent testimony: any misreading baked
into a formalization is likely repeated in its read-back, and agreement between the two should
not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own
first paragraph. Reviewers who want independent testimony should commission fresh, blind
read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`): all files
elaborate with no errors, the only warnings being the expected `sorry` placeholders in the
theorem bodies.
Ideals in Balanced Algebras: the Gregarious IdealResearch Paper
## Motivation
A recurring pattern in algebra is that a structure is analysed through distinguished subobjects — normal subgroups, ring ideals, submodules — and that requiring those subobjects to be trivial isolates the sharply defined classes (simple groups, division rings, simple modules) about which the deepest theorems are available. The manuscript *Ideals in Balanced Algebras and the Genesis of Mathematics* (A. Winkler, 2020) applies that pattern to a single primitive: a **partial binary operation**, an operation $a\cdot b$ that need not be defined for every pair. Under one axiom — **balance**, which asserts that $(ab)c$ is defined exactly when $a(bc)$ is — several families of ideals appear automatically, and declaring each of them trivial (empty, or the whole algebra) carves out semigroups, monoids, quivers, associations, societies, categories, groupoids, groups and rings in turn.
No individual argument here is deep. What makes them worth machine-checking is that their content is *definedness* rather than equality: a statement such as "the gregarious elements form an ideal" is a claim about which products exist, proved by repeatedly moving brackets across a product that may fail to be defined at any step. Such arguments are easy to state loosely, and easy to get wrong by one implicit existence assumption. They are also the base layer on which the rest of the manuscript's programme rests. This mission formalizes that base layer: §1 (algebras, ideals, units), §2 (quivers), §4 (associators and associations), §4.1 (principal ideals) and §4.2 (the gregarious ideal).
## Setting
An **algebra** on a type $A$ is a partial binary operation: a rule assigning to some pairs $(a,b)\in A\times A$ a value $a\cdot b\in A$. Write $a\cdot b\downarrow$ for "$a\cdot b$ is defined". In the Lean development the operation is a total function $A\to A\to\mathrm{Option}\,A$, where the value $\mathrm{none}$ means undefined. Nothing else is assumed: no totality, no unit, no associativity.
The vocabulary used throughout, all relative to this one partial product:
1. $B\subseteq A$ is a **left ideal** if $a\cdot b\in B$ whenever $b\in B$ and $a\cdot b\downarrow$; a **right ideal** if $b\cdot a\in B$ whenever $b\in B$ and $b\cdot a\downarrow$; a **subalgebra** if $b\cdot c\in B$ whenever $b,c\in B$ and $b\cdot c\downarrow$.
2. The **right orbit** of $a$ is $aA=\{c:\exists b,\ a\cdot b=c\}$; the left orbit is dual.
3. The algebra is **balanced** if, for all $a,b,c$, $(a\cdot b)\cdot c$ is defined if and only if $a\cdot(b\cdot c)$ is.
4. $u$ is a **left unit** if $u\cdot a=a$ whenever $u\cdot a\downarrow$, and $v$ is a **right unit** if $a\cdot v=a$ whenever $a\cdot v\downarrow$. A left unit $u$ is a **source** if $a\cdot u\downarrow$ only for $a=u$; a right unit $v$ is a **sink** if $v\cdot b\downarrow$ only for $b=v$.
5. $b$ is **associating** if for all $a,c$ the product $(ab)c$ is defined exactly when $a(bc)$ is, and the two values agree whenever both are defined. An **association** is an algebra all of whose elements are associating.
6. $b$ is **gregarious** if, whenever $a\cdot b\downarrow$ and $b\cdot c\downarrow$, at least one of $(ab)c$ and $a(bc)$ is defined. An association that coincides with its set of gregarious elements is a **society**; in the manuscript's terms, a quivered society is a category.
7. $b$ is **left cancellable** if $b\cdot x=b\cdot y$, with both sides defined, forces $x=y$.
## Formalization targets
### Goal — the gregarious ideal (§4.2)
$$\text{If } A \text{ is an association, then } \{\,b\in A: b \text{ is gregarious}\,\} \text{ is both a left ideal and a right ideal.}$$
This is the statement that gives the manuscript its notion of *society*: the gregarious elements of an association form the **gregarious ideal**, and an association whose gregarious ideal is everything is a society. The goal fixes no cardinality, no units and no totality, so it survives every specialization the manuscript makes afterwards.
### Supporting targets
The milestone list works up to the goal through the manuscript's own intermediate claims: the orbit characterization of right ideals and the elementary facts about units (§1); the two derived quiver identities (§2); closure of the associating elements under the product (§4); principal right ideals (§4.1); gregariousness of sinks and sources, and the two one-sided closure statements for gregarious associating elements (§4.2); and the cancellation facts (§4) whose content is that the non-left-cancellable elements form a prime left ideal.
## Significance
The result itself gives the manuscript's structural dichotomy a stable base. Once the gregarious elements are known to form an ideal, "society" is a triviality condition on an ideal rather than an ad hoc axiom, and the same is true of *quivered* (the elements admitting a unit on one side form an ideal, §1), of *cancellative* (the non-cancellable elements form a prime ideal, §4) and of *principal* (§4.1). The chain of specializations the manuscript then runs — association, society, quivered society, category, groupoid, group, ring — inherits whatever is proved here.
What this mission adds on top of the manuscript is machine-checked bookkeeping for partial operations. The arguments in the source are written in prose, with the existence of intermediate products often left implicit; formalizing them fixes exactly which existence facts each step consumes. The definitions published with this mission (partial algebra, ideal, balance, associating, gregarious, unit, source, sink, cancellable) are reusable for any later formalization of partial magmas, and nothing equivalent is currently in Mathlib, whose `Magma`-style structures are total and whose `Quiver`/`Category` hierarchy starts from typed hom-families rather than a single partial product.
## Difficulty
The obstacle is uniform and easy to underestimate: in a partial algebra one may never assume that a product written down in the course of an argument exists. The naive proof of the goal — "rebracket and apply gregariousness of $b$" — fails at its first step, because from $a\cdot(bc)\downarrow$ alone one cannot conclude $a\cdot b\downarrow$; that inference is exactly what the hypothesis "$b$ is associating" supplies, and it must be invoked explicitly. Gregariousness then returns a disjunction whose two branches produce products on opposite sides of the bracket, so each branch has to be transported back independently, consuming a further associating hypothesis. Counting these obligations correctly, rather than inventing new mathematics, is the work.
## Formalization scope
The partial product is `A → A → Option A`; `none` is undefined, and `a · b = c` is rendered as the product evaluating to `some c`. Subsets are `Set A`, with no decidability or finiteness assumptions. Ideals are arbitrary subsets and are allowed to be empty — deliberately, since the manuscript's dichotomy turns on an ideal being empty or being everything. Statements quantify over an arbitrary type, including the empty type, where they hold vacuously.
Left/right duality is not obtained from a formal opposite-algebra construction: the dual statements are stated and are to be proved separately (for instance the two one-sided society closure milestones). A contributor who prefers to build the opposite algebra once and derive each dual from its mirror is welcome to; that construction is not part of the published definitions.
The statements are not vacuous: every hypothesis used is satisfiable, since any total associative operation makes all elements associating and gregarious, and the trivial one-element monoid satisfies every unit, source, sink and cancellation hypothesis appearing in the list. No milestone is stated under a hypothesis that cannot be met.
## Selected references
- A. Winkler, *Ideals in Balanced Algebras and the Genesis of Mathematics*, manuscript, 20 March 2020. Source text supplied by the mission owner; section and page references in the items below are to that manuscript.
- S. Eilenberg and S. Mac Lane, *General theory of natural equivalences*, Transactions of the American Mathematical Society 58 (1945), 231–294. https://doi.org/10.1090/S0002-9947-1945-0013131-6
Gelbart's Langlands Survey I: Hecke's Correspondence between Automorphic Forms and Dirichlet SeriesResearch Paper
## Motivation
The Langlands program proposes that the arithmetic of number fields is encoded in the
representation theory of reductive groups over their adele rings. Its conjectures — reciprocity
and functoriality — are stated in the survey this mission formalizes,
[Gelbart 1984](https://doi.org/10.1090/S0273-0979-1984-15237-6), only after a long preparatory
part on the classical results they generalize, and it is that classical part (Part II of the
survey) that admits precise formal statements today.
The classical engine is a theorem of **Hecke** (1936): a holomorphic function on the upper
half-plane, given by a Fourier expansion in $e^{2\pi i n z/h}$, transforms in a prescribed way
under $z \mapsto -1/z$ **exactly when** the Dirichlet series built from its Fourier coefficients
continues analytically and satisfies a functional equation. One side of the equivalence is a
symmetry of an analytic object on the upper half-plane; the other is an analytic property of a
series assembled from arithmetic data. Gelbart presents this as the prototype of the
"reciprocity" that the Langlands conjectures extend to $GL_n$ and beyond.
Timeline of the material covered here.
- 1859: Riemann derives the functional equation of $\zeta(s)$ from the transformation law of the
Jacobi theta function, via the Mellin transform (Gelbart, §II.B.2, p. 187).
- 1920s: Hasse and Minkowski establish the local-global principle for rational quadratic forms
(Gelbart, §II.A, p. 186).
- 1936: Hecke proves the equivalence that is this mission's goal, and characterizes Euler
products among Dirichlet series of automorphic forms (Gelbart, §II.B.2, Theorems 1 and 2).
- 1967: Weil extends Hecke's theorem to congruence subgroups; Langlands formulates functoriality.
## Setting
Fix a sequence of complex numbers $a_0, a_1, a_2, \dots$ subject to the growth condition
$a_n = O(n^c)$ for some $c > 0$, a period $h > 0$, a weight $k > 0$, and a sign $C = \pm 1$.
Three objects are attached to this data.
- The **form**: $\displaystyle f(z) = \sum_{n \ge 0} a_n e^{2\pi i n z/h}$, holomorphic on the
upper half-plane $\{z : \operatorname{Im} z > 0\}$.
- The **Dirichlet series**: $\displaystyle \varphi(s) = \sum_{n \ge 1} \frac{a_n}{n^s}$,
absolutely convergent for $\operatorname{Re} s > c+1$.
- The **completed series**:
$\displaystyle \Phi(s) = \left(\frac{2\pi}{h}\right)^{-s} \Gamma(s)\, \varphi(s)$.
Two conditions on this data are compared.
$$\textbf{(A)}\quad \Phi(s) + \frac{a_0}{s} + \frac{C a_0}{k-s} \ \text{extends to an entire
function, bounded in every vertical strip, and}\ \Phi(k-s) = C\,\Phi(s).$$
$$\textbf{(B)}\quad f(-1/z) = C\left(\frac{z}{i}\right)^{k} f(z) \qquad (\operatorname{Im} z > 0).$$
Condition (B) says that $f$ is automorphic of weight $k$ for the group of transformations
generated by $z \mapsto z + h$ and $z \mapsto -1/z$; invariance under $z \mapsto z+h$ is built
into the Fourier expansion.
## Formalization targets
### Goal — Theorem 1 (Hecke), p. 188
$$\textbf{(A)} \iff \textbf{(B)}$$
for every coefficient sequence of polynomial growth and all $h, k > 0$, $C = \pm 1$. The goal
fixes no particular group, no level and no arithmetic input: it is the general equivalence, from
which the classical examples follow by specialization.
### Milestones
The milestone list follows the survey: the local-global principle of §II.A, the Riemann–theta
computation that motivates Hecke's proof (§II.B.2, p. 187), the Mellin representation of $\Phi$,
the two implications of Theorem 1 separately, and the Euler-product criterion of Theorem 2
(p. 189).
## Significance
Hecke's theorem is what makes "this $L$-function is automorphic" a checkable assertion: it
converts a statement about analytic continuation and a functional equation — often the only
handle one has on an arithmetically defined Dirichlet series — into the existence of an
automorphic form with prescribed Fourier coefficients. Weil's converse theorem, the modularity of
elliptic curves, and the automorphy criteria used throughout the Langlands program are
descendants of this statement. Downstream of it sit the classical applications listed in the
survey: the functional equations of $\zeta$ and of Dirichlet $L$-functions, and the
identification of theta series of quadratic forms with modular forms.
Status. Hecke's theorem is a classical, fully proved result (Hecke 1936; a textbook treatment is
Ogg, *Modular forms and Dirichlet series*, Ch. 1). Hasse–Minkowski is likewise classical. Neither
has a formalization in Mathlib at the pinned revision: Mathlib supplies the completed Riemann
zeta function and its functional equation, the Jacobi theta transformation law, `LSeries` and its
abscissa theory, the Gamma function and the Mellin transform, and modular forms with
`SlashAction`, but no converse theorem and no local-global principle for quadratic forms. What
this mission produces is therefore new formal mathematics on top of an old result, not a
re-derivation of something already machine-checked.
## Difficulty
The forward implication (B) $\Rightarrow$ (A) is Riemann's argument: split
$\int_0^\infty (f(iy) - a_0) y^{s-1}\,dy$ at $y = 1$, substitute $y \mapsto 1/y$ in the lower
piece, and use (B). The obstacle is not the algebra but the analysis that licenses it: exchanging
the sum defining $f$ with the integral, controlling $f(iy) - a_0$ as $y \to 0^{+}$, where the
naive termwise bound diverges, and showing the result is entire *and* bounded on vertical strips
rather than merely holomorphic on a half-plane.
The reverse implication (A) $\Rightarrow$ (B) is harder, and it is where the first idea fails: one
cannot simply run the computation backwards, because the Mellin inversion integral
$\frac{1}{2\pi i}\int_{(\sigma)} \Phi(s) y^{-s}\,ds$ converges only once boundedness in vertical
strips is combined with Stirling decay of $\Gamma$, and the contour shift that produces the $a_0$
terms needs both. Mathlib has the Mellin transform and an inversion theorem, under hypotheses that
are not met verbatim here; supplying that bridge is the main work.
## Formalization scope
Conventions committed to in Lean, all of them invisible in the prose.
- $f$ is defined as an unconditional `tsum` over $n \ge 0$, so it takes the junk value $0$ where
the series fails to converge; every statement about $f$ is guarded by $\operatorname{Im} z > 0$,
and a separate item asserts summability there.
- $\varphi$ is Mathlib's `LSeries`, whose $n = 0$ term is $0$ by definition, so $a_0$ never enters
the Dirichlet series — only the correction terms $a_0/s$ and $C a_0/(k-s)$.
- "Entire" is rendered as differentiability on all of $\mathbb{C}$; "bounded in every vertical
strip" as: for all reals $\sigma_1, \sigma_2$ there is an $M$ bounding the function on
$\sigma_1 \le \operatorname{Re} s \le \sigma_2$.
- The functional equation is imposed on the *continued* function $F$ as $F(k-s) = C\,F(s)$; for
$C = \pm 1$ this is equivalent to $\Phi(k-s) = C\,\Phi(s)$ on the half-plane of convergence.
- Complex powers $(2\pi/h)^{-s}$, $(z/i)^{k}$ and $y^{s-1}$ are principal-branch `cpow`; on the
upper half-plane $z/i$ has positive real part, so no branch ambiguity arises.
- The growth hypothesis is $\lVert a_n \rVert \le K n^{c}$ for $n \ge 1$ with $c > 0$, and the
abscissa used throughout is $\sigma = c+1$.
- The printed source reads $\Phi(s) + a_0/s + C/(k-s)$; the term $C a_0/(k-s)$ used here is the
standard form of the correction (see Ogg, Ch. 1), and the two agree when $a_0 = 0$.
No trivializing reading is available: condition (A) requires the entire function to *agree with*
$\Phi(s) + a_0/s + C a_0/(k-s)$ on $\operatorname{Re} s > c+1$, where $\Phi$ is genuinely defined,
so it is not satisfied by an arbitrary entire function; and the hypotheses of the goal are
satisfiable — the Jacobi theta coefficients with $h = 2$, $k = 1/2$, $C = 1$ are an instance,
recorded as its own item.
A complete development needs: summability and holomorphy of $q$-expansions of polynomial growth;
the Mellin transform of an exponentially decaying series; entirety and strip-boundedness of the
continued $\Phi$; Mellin inversion with Stirling control of $\Gamma$; and, for the Euler-product
item, the passage from multiplicativity to an Euler product for `LSeries`. All of these are
reusable beyond this mission. Contributions to any single item are welcome; the two implications
of the goal are independently valuable and are listed as separate milestones for that reason.
## Selected references
- S. Gelbart, *An elementary introduction to the Langlands program*, Bull. Amer. Math. Soc. (N.S.)
**10** (1984), 177–219. https://doi.org/10.1090/S0273-0979-1984-15237-6
- E. Hecke, *Über die Bestimmung Dirichletscher Reihen durch ihre Funktionalgleichung*, Math. Ann.
**112** (1936), 664–699. https://doi.org/10.1007/BF01565437
- A. Ogg, *Modular forms and Dirichlet series*, W. A. Benjamin, 1969.
- R. P. Langlands, *Problems in the theory of automorphic forms*, Lectures in Modern Analysis and
Applications III, Lecture Notes in Math. **170** (1970), 18–61.
https://doi.org/10.1007/BFb0079065
- J.-P. Serre, *A course in arithmetic*, Springer GTM 7, 1973 (Ch. IV: Hasse–Minkowski).
## A.L.E.T.H.E.A.N. — the engine behind this corpus
This mission curates the formalized output of [**Alethean**](https://alethean.org) — an *Autonomous Logic Engine for Theorem Hunting, Exploration, And Navigation* ([alethean.org](https://alethean.org)). Alethean autonomously generates research directions, develops them into research papers, and formalizes their results in Lean 4 — an "ever-expanding registry of absolute mathematical truths," built with the [Aristotle](https://aristotle.harmonic.fun) reasoning engine. *"The unconcealed truth between conjecture and proof."*
The corpus's public home is the [Alethean Lean 4 Catalog](https://alethean.org) — the central registry of formalized theorems across the ecosystem, browsable as **research packages** (each with its article, research paper, interactive view, future directions, and Lean 4 proof files). This mission is the platform-side mirror of that registry: **2,799 definition bundles and 7,517 theorems** compiled and verified against the pinned toolchain (Lean v4.30.0, Mathlib `c5ea003`), spanning analytic number theory, combinatorics, probability, information theory, quantum information, tropical algebra, and machine-learning theory.
## What is being asked
The corpus arrives **fully proved**. The goal theorem is the corpus's universal error-detection bound for random checksums — the capstone of the Almost-Lossless compression thread (*Compression Beyond the Pigeonhole Bound*): appending an independent random checksum makes the probability of silent corruption at most $1/K$, uniformly over all source strings and *all* inner decoders. The milestones are capstone theorems from across the corpus: sphere-packing and VC-dimension bounds, second moments of central $L$-values, tropical Arrow-type impossibility, sums-of-three-cubes obstructions, and more.
## For solvers
Every milestone is a verified platform theorem: study the proofs, reuse them as imported lemmas, or rebuild them from first principles. The interesting open work is **extension**: the corpus's research-direction papers (browsable at [alethean.org](https://alethean.org) under *Future Directions*) state quantitative sharpenings — explicit constants, wider parameter ranges — that are not yet formalized. Pick a direction, formalize its statement, and the verification pipeline does the rest.
## Provenance
- Source repository: [github.com/raver1975/lean](https://github.com/raver1975/lean) (commit `53c2925a02`)
- Public registry: [alethean.org](https://alethean.org)
- Toolchain: Lean v4.30.0, Mathlib `c5ea00351c28e24afc9f0f84379aa41082b1188f`
- All uploaded items are tagged `aether-catalog`.
Grothendieck-Teichmüller: the graded Lie algebra grt_1 and the Deligne-Drinfeld-Ihara conjectureOpen Problem
## Motivation
The **Grothendieck-Teichmüller group** organises a family of symmetries that act on braided
monoidal categories, on quantised universal enveloping algebras, on the little-discs operad, and
on the ring of periods of the projective line minus three points. Three versions exist: a
profinite one $\widehat{GT}$, introduced by Grothendieck and Drinfeld and containing the absolute
Galois group $\mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)$; a pro-$\ell$ one; and a
pro-unipotent one $GT$, together with its graded companion $GRT$. This mission is about the
graded, pro-unipotent side, which is the version that governs the homological-algebra and
deformation-quantisation applications, and which is closest to a concrete, computable object: a
Lie algebra of Lie polynomials in two variables, cut out by three explicit equations.
Its Lie algebra $\mathfrak{grt}_1$ carries a distinguished family of elements
$\sigma_3, \sigma_5, \sigma_7, \dots$, one in each odd degree at least $3$, produced from the
Knizhnik-Zamolodchikov associator. **Deligne, Drinfeld and Ihara** conjectured that
$\mathfrak{grt}_1$ is the free Lie algebra on such a family. A timeline of what is actually
known:
* 1990 - V. Drinfeld, *On quasitriangular quasi-Hopf algebras and a group closely connected with
$\mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)$*, introduces $GT$, $GRT$, associators, and the
defining equations of $\mathfrak{grt}_1$; the Knizhnik-Zamolodchikov associator shows the set
of associators is non-empty, hence $\sigma_3, \sigma_5, \dots$ exist and are non-zero.
* 2012 - F. Brown, *Mixed Tate motives over $\mathbb Z$* (Annals of Mathematics 175, 949-976,
[doi:10.4007/annals.2012.175.2.10](https://doi.org/10.4007/annals.2012.175.2.10)), proves that
the $\zeta^{\mathfrak f}(r_1,\dots,r_n)$ with $r_j \in \{2,3\}$ form a basis of the algebra of
motivic multiple zeta values. One half of the conjecture follows: the Lie subalgebra of
$\mathfrak{grt}_1$ generated by the $\sigma_{2p+1}$ is free on them.
* The converse half - that these elements generate all of $\mathfrak{grt}_1$ - is open.
## Setting
Let $\mathbb{F}(x,y)$ be the free Lie algebra over $\mathbb Q$ on two generators $x$ and $y$,
graded by total word length. For a Lie algebra $A$ over $\mathbb Q$ and $a, b \in A$, write
$\psi(a,b)$ for the image of $\psi \in \mathbb{F}(x,y)$ under the unique Lie algebra morphism
sending $x \mapsto a$ and $y \mapsto b$.
For $n \ge 1$, the **Drinfeld-Kohno Lie algebra** $\mathfrak t_n$ is generated over $\mathbb Q$
by symbols $t_{ij}$, $1 \le i, j \le n$, subject to
$$t_{ii} = 0, \qquad t_{ij} = t_{ji}, \qquad [t_{ij}, t_{kl}] = 0, \qquad
[t_{ij}, t_{ik} + t_{jk}] = 0,$$
the third relation for $i,j,k,l$ pairwise distinct and the fourth for $i,j,k$ pairwise distinct.
It is the Lie algebra of infinitesimal braid relations: the associated graded of the pure braid
Lie algebra, and the coefficient algebra of the Knizhnik-Zamolodchikov connection.
The **graded Grothendieck-Teichmüller Lie algebra** $\mathfrak{grt}_1$ is the set of
$\psi \in \mathbb{F}(x,y)$ satisfying three equations:
$$\psi(x,y) = -\psi(y,x),$$
$$\psi(x,y) + \psi(y,z) + \psi(z,x) = 0 \quad \text{where } x + y + z = 0,$$
$$\psi(t_{12},t_{23}) - \psi(t_{12},t_{23}+t_{24}) + \psi(t_{12}+t_{13},t_{24}+t_{34})
- \psi(t_{13}+t_{23},t_{34}) + \psi(t_{23},t_{34}) = 0 \ \text{ in } \mathfrak t_4 .$$
All three are linear in $\psi$ and degree preserving, so $\mathfrak{grt}_1$ is a graded
$\mathbb Q$-subspace.
$\mathfrak{grt}_1$ is *not* closed under the bracket of $\mathbb{F}(x,y)$; it is closed under the
**Ihara (Poisson) bracket**
$$\{f,g\} = [f,g] + D_f g - D_g f,$$
where $D_f$ is the derivation of $\mathbb{F}(x,y)$ determined by $D_f x = 0$ and
$D_f y = [y,f]$. Writing $\mathrm{Der}$ for the Lie algebra of derivations of $\mathbb{F}(x,y)$
under the commutator, the assignment $f \mapsto D_f$ satisfies
$[D_f, D_g] = D_{\{f,g\}}$, and it is injective on $\mathfrak{grt}_1$; this is the form in which
the Lie structure of $\mathfrak{grt}_1$ is expressed in the formal statements below.
Finally, for $n_1 \ge 2$ and $n_2,\dots,n_k \ge 1$ the **multiple zeta value** is
$$\zeta(n_1,\dots,n_k) = \sum_{j_1 > j_2 > \cdots > j_k \ge 1}
\frac{1}{j_1^{n_1} j_2^{n_2} \cdots j_k^{n_k}} .$$
These numbers are the coefficients of the Knizhnik-Zamolodchikov associator, which is why they
enter a mission about $\mathfrak{grt}_1$; they satisfy the stuffle and shuffle relations, whose
common refinement (the double shuffle relations) is the arithmetic side of the same story.
## Formalization targets
### Goal - Deligne-Drinfeld-Ihara
$$\exists\, \sigma_0, \sigma_1, \sigma_2, \dots \in \mathfrak{grt}_1, \quad
\deg \sigma_p = 2p+3, \quad \text{such that } \mathfrak{grt}_1 \text{ is the free Lie algebra}
\text{ on } (\sigma_p)_{p \ge 0} \text{ for } \{\,,\}.$$
Concretely: the Lie algebra morphism from the free Lie algebra on countably many generators to
$\mathrm{Der}$ sending the $p$-th generator to $D_{\sigma_p}$ is injective, and its image is
exactly $D(\mathfrak{grt}_1)$. The statement fixes the degrees of the generators but not the
generators themselves, which is the weakest form that still carries the content of the
conjecture.
### Milestone level - Brown's half
The same family exists with the morphism merely **injective**: the $\sigma_{2p+1}$ generate a
free Lie subalgebra. This is a theorem (Brown 2012); the open part of the goal is surjectivity.
### Supporting levels
The Ihara bracket is a Lie bracket; $\mathfrak{grt}_1$ is closed under it; the degree-$3$ element
$[x+y,[x,y]]$ lies in $\mathfrak{grt}_1$; every odd degree $\ge 3$ contains a non-zero element of
$\mathfrak{grt}_1$; multiple zeta values satisfy the stuffle and shuffle relations; and
$\zeta(2,1) = \zeta(3)$.
## Significance
A positive answer would determine $\mathfrak{grt}_1$ completely and, through the
$GT$-$GRT$-associator torsor, describe the pro-unipotent Grothendieck-Teichmüller group by
generators without relations. Downstream it would pin down the homotopy automorphisms of the
rationalised little-discs operad and the Lie algebra of the motivic Galois group of mixed Tate
motives over $\mathbb Z$ up to the same freeness statement. Without it, even the dimension of
$\mathfrak{grt}_1$ in a given degree is only known to be bounded above by the Broadhurst-Kreimer
style count, with equality unproved.
Formalizing this mission produces a machine-checked definition of $\mathfrak t_n$,
$\mathfrak{grt}_1$ and the Ihara bracket - objects that have no Mathlib counterpart at present -
and machine-checked proofs of the Lie-theoretic facts around them. Brown's theorem itself is
proved in the literature but not formalized; the goal statement is genuinely open, and no part
of this mission is closed by an existing Lean development known to the proposal.
## Difficulty
The obvious approach to the goal - exhibit the generators and count dimensions degree by degree -
fails in both directions. Upwards, no closed formula for $\sigma_{2p+1}$ is known: they are
extracted from the Knizhnik-Zamolodchikov associator, whose coefficients are regularised iterated
integrals, and only their leading coefficients are controlled. Downwards, freeness of the
subalgebra they generate is not an algebraic manipulation of the three defining equations: Brown
derives it from the motivic theory of multiple zeta values, where the missing input is a basis
theorem for a period algebra, not an identity in $\mathbb{F}(x,y)$. Even the milestone
"$\mathfrak{grt}_1$ is closed under the Ihara bracket" is not a formality: the pentagon equation
lives in $\mathfrak t_4$ and must be transported through substitutions into a quotient Lie
algebra.
## Formalization scope
The formalization commits to the following conventions, all visible in the definition files.
1. The base field is $\mathbb Q$. The source works over a field $K$ of characteristic zero; every
statement here is over $\mathbb Q$.
2. $\mathfrak{grt}_1$ is modelled inside the **free Lie algebra** `FreeLieAlgebra ℚ (Fin 2)`,
i.e. by Lie *polynomials*, not the completed Lie algebra $\widehat{\mathbb{F}}(x,y)$ of the
source. The three defining equations are homogeneous, so the graded object determines the
completed one; solvers should be aware that no topology or completion appears anywhere.
3. $\mathfrak t_n$ is the quotient of the free Lie algebra on ordered pairs of indices in
`Fin n` by the Lie ideal generated by the four relation families above, so `dkGen i j` is
$t_{i+1,j+1}$ under the shift `Fin 4 = {0,1,2,3}` versus indices $1,2,3,4$.
4. Homogeneity is expressed by the rescaling characterisation: $\psi$ has degree $n$ if
$\psi(cx,cy) = c^n \psi(x,y)$ for all $c \in \mathbb Q$. Over an infinite field this is
equivalent to homogeneity for the word-length grading.
5. The Ihara derivation uses $D_f x = 0$. The source writes $D_f x = x$ in Remark 4.4 and in
Section 7.3, but that convention contradicts Lemma 7.2 of the same notes and the computation
$\{x,y\} = [x,y] + [y,x] = 0$ in Remark 7.2; $D_f x = 0$ is the convention under which both
hold, and is the standard one.
6. The Lie structure on $\mathfrak{grt}_1$ is carried by the injection $f \mapsto D_f$ into
`LieDerivation ℚ (FreeLieAlgebra ℚ (Fin 2)) (FreeLieAlgebra ℚ (Fin 2))`, so that freeness can
be stated as injectivity of a morphism out of a free Lie algebra without first installing a
new Lie algebra structure. Note $f \mapsto D_f$ is injective on $\mathfrak{grt}_1$ but not on
all of $\mathbb{F}(x,y)$, where $D_y = 0$; a supporting item records the injectivity actually
used.
7. Multiple zeta values are real numbers defined by an iterated `tsum`; for non-admissible words
the series diverges and the definition returns Mathlib's junk value. Every statement about
them therefore carries an admissibility hypothesis: all letters $\ge 1$ and first letter
$\ge 2$. The stuffle and shuffle products are multisets of words, so no free module on words
is needed.
8. Nothing here is vacuous by construction: the defining equations of $\mathfrak{grt}_1$ are
linear conditions on a non-zero graded space, $\mathfrak t_4 \ne 0$, and the milestone
$[x+y,[x,y]] \in \mathfrak{grt}_1$, $[x+y,[x,y]] \ne 0$ exhibits a non-zero element.
Contributions welcome: the Lie-theoretic milestones (Lemma 7.2, Corollary 7.1, closure of
$\mathfrak{grt}_1$, the degree-$3$ element) are self-contained and need no motivic input; the
multiple zeta milestones need summability infrastructure for iterated series; Brown's theorem and
the goal need a substantial development that does not yet exist in Lean.
## Selected references
* V. G. Drinfeld, *On quasitriangular quasi-Hopf algebras and a group closely connected with*
$\mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)$, Leningrad Math. J. 2 (1991), 829-860.
* F. Brown, *Mixed Tate motives over* $\mathbb Z$, Annals of Mathematics 175 (2012), 949-976,
[doi:10.4007/annals.2012.175.2.10](https://doi.org/10.4007/annals.2012.175.2.10).
* T. Willwacher, *The Grothendieck-Teichmüller Group*, ETH Zürich lecture notes, 27 February
2014 (the source text for this mission).
* T. Willwacher, *M. Kontsevich's graph complex and the Grothendieck-Teichmüller Lie algebra*,
Invent. Math. 200 (2015), 671-760,
[doi:10.1007/s00222-014-0528-x](https://doi.org/10.1007/s00222-014-0528-x).
## Motivation
The **spectral gap** of a quantum many-body Hamiltonian is the difference between the energy of its ground state and the energy of its first excited state, in the limit of infinitely many particles. Whether a given microscopic interaction produces a gapped or a gapless system decides much of the macroscopic physics: gapped systems have exponentially decaying correlations and well-defined quantum phases, gapless systems sit at critical points and can display algebraically decaying correlations. Several long-standing questions — the **Haldane conjecture** for antiferromagnetic spin chains, the existence of gapped topological spin liquids, and the **Yang–Mills mass gap** — are instances of the question "given the interaction, is the system gapped?".
Cubitt, Pérez-García and Wolf proved that this question, posed for families of two-dimensional translationally invariant nearest-neighbour spin models, admits no algorithmic answer: the **spectral gap problem is undecidable** ([Nature 528, 207–211 (2015)](https://doi.org/10.1038/nature16059); full version: [Forum of Mathematics, Pi 10:e14 (2022)](https://doi.org/10.1017/fmp.2021.15), also [arXiv:1502.04573](https://arxiv.org/abs/1502.04573)).
Timeline of the ingredients the proof rests on: Turing's undecidability of the halting problem (1936); Berger's undecidability of the domino problem (1966) and Robinson's aperiodic tile set ([Inventiones 12, 177–209 (1971)](https://doi.org/10.1007/BF01418780)); Feynman's and Kitaev's circuit-to-Hamiltonian constructions, which turn a computation into a ground state; Gottesman and Irani's translationally invariant one-dimensional Hamiltonians encoding computation ([FOCS 2009](https://arxiv.org/abs/0905.2419)); and Bitansky–Vadhan-style quantum Turing machine engineering from Bernstein and Vazirani ([SIAM J. Comput. 26, 1411–1473 (1997)](https://doi.org/10.1137/S0097539796300921)). The 2015 result was later sharpened to one-dimensional chains by Bausch, Cubitt, Lucia and Pérez-García ([PRX 10, 031038 (2020)](https://doi.org/10.1103/PhysRevX.10.031038)).
## Setting
Fix a local dimension $d$ and, for each side length $L$, the square lattice $\Lambda(L)=\{1,\dots,L\}^2$ with **open boundary conditions**. Each site carries a copy of $\mathbb{C}^d$, so the state space of the lattice has the standard product basis indexed by assignments of a level in $\{1,\dots,d\}$ to each site. A model is specified by three Hermitian matrices: an on-site term $h_1$ of size $d\times d$, and two interactions $h_{\mathrm{row}},h_{\mathrm{col}}$ of size $d^2\times d^2$ acting on horizontally and vertically adjacent pairs. The Hamiltonian of the finite lattice is
$$H^{\Lambda(L)} \;=\; \sum_{\text{horizontal edges}} h_{\mathrm{row}}^{(i,j)} \;+\; \sum_{\text{vertical edges}} h_{\mathrm{col}}^{(i,j)} \;+\; \sum_{k\in\Lambda(L)} h_1^{(k)},$$
the same three matrices being used at every edge and every site, which is what **translational invariance** means here. The quantity $\max\{\|h_1\|,\|h_{\mathrm{row}}\|,\|h_{\mathrm{col}}\|\}$ is the **local interaction strength**.
Write $\lambda_0(H^{\Lambda(L)})\le\lambda_1(H^{\Lambda(L)})\le\cdots$ for the eigenvalues and $\Delta(H^{\Lambda(L)})=\lambda_1-\lambda_0$ for the finite-size gap. The family $\{H^{\Lambda(L)}\}_L$ is
- **gapped** (Definition 1 of the source) if there are $\gamma>0$ and $L_0$ such that for all $L>L_0$ the ground state of $H^{\Lambda(L)}$ is non-degenerate and $\Delta(H^{\Lambda(L)})\ge\gamma$;
- **gapless** (Definition 2 of the source) if there is $c>0$ such that for every $\varepsilon>0$ there is an $L_0$ with: for all $L>L_0$, every point of $[\lambda_0,\lambda_0+c]$ lies within $\varepsilon$ of the spectrum of $H^{\Lambda(L)}$.
These two conditions are not negations of each other; the construction guarantees that every instance falls into one of them. The **ground state energy density** is $E_\rho=\lim_{L\to\infty}\lambda_0(H^{\Lambda(L)})/L^2$.
## Formalization targets
### Goal — Theorem 3 of the source
For a fixed universal machine and every $n$, one explicit family of interactions, built from fixed integer-valued matrices $A,A',B,C,D,D'$, a diagonal projector $\Pi$, a rational $\beta>0$ that may be taken arbitrarily small, and an algebraic $\alpha(n)\le 2\beta$,
$$h_1(n)=\alpha(n)\Pi,\qquad h_{\mathrm{col}}(n)=D+\beta D',$$
$$h_{\mathrm{row}}(n)=A+\beta\Bigl(A'+e^{i\pi\varphi}B+e^{-i\pi\varphi}B^{\dagger}+e^{i\pi 2^{-|\varphi|}}C+e^{-i\pi 2^{-|\varphi|}}C^{\dagger}\Bigr),$$
with $\varphi=\varphi(n)$ the rational whose binary expansion after the point is the binary expansion of $n$ reversed, satisfies: the local interaction strength is at most $1$; if the machine halts on input $n$ the family is gapped with gap at least $1$; and if it does not halt the family is gapless. Since halting is undecidable, no algorithm decides gappedness, even with the promise that exactly one of the two alternatives holds and even at fixed local dimension $d$.
### Milestones
The milestone list follows the numbering of the full version: Lemma 8 and Theorem 9 (reduction of halting to ground state energy and to arbitrary low-energy properties), Corollary 7 (the same undecidability for unconstrained local dimension, with rational interactions), Proposition 53 and Corollary 54 (the diverging ground state energy and its promise version), and Theorem 5 (undecidability of the ground state energy density).
## Significance
The result rules out a general algorithm — and therefore any complete general method — for deciding gappedness from the interaction matrices, however much computing power is available; the property genuinely depends on arbitrarily large system sizes. It also implies, via the standard link between undecidability and independence, that there are concrete finite-dimensional models whose gap is independent of the axioms of any consistent recursively axiomatized formal system (Corollary 4 of the source), and it transfers to other low-energy properties such as the existence of algebraically decaying ground-state correlations.
The theorem is proved; none of it is formalized. This mission produces the machine-checked version. The reusable infrastructure it forces into existence is substantial on its own: a formal model of translationally invariant lattice Hamiltonians and their thermodynamic-limit spectral behaviour, the tiling layer, and computational-history-state Hamiltonians. Each milestone is a self-contained statement that can be attacked without the others.
## Difficulty
The obvious approach — encode a halting computation as an energy penalty — gives the ground state *energy* of a finite lattice, not a property of the limit; this is exactly what Lemma 8 achieves, and it is not enough, because a gap is a statement about the sequence of spectra as $L\to\infty$ and is insensitive to any single lattice size. The construction must make the halting information visible at *all* sufficiently large sizes at once while a fixed finite local dimension carries every instance $n$. That forces three separate difficulties: an aperiodic (Robinson) tiling to create squares of every size $2^n$ inside one translationally invariant model; a quantum phase-estimation Turing machine whose transition amplitudes encode $n$ in a single phase $e^{i\pi\varphi(n)}$, so that the instance index does not inflate the local dimension; and a history-state Hamiltonian whose low-energy spectrum can be controlled well enough that a positive energy density in the halting case turns into a genuine spectral gap, and a vanishing one into a dense spectrum above the ground state.
## Formalization scope
The development commits to the following conventions, all of which are visible in the definition items of this mission.
1. Lattices are finite: sites are pairs of indices in $\{0,\dots,L-1\}$, edges are consecutive pairs within a row or a column (**open boundary conditions**; the periodic case of Section 6.3 of the source is out of scope).
2. Operators are complex matrices indexed by product-basis configurations; the interactions are embedded by acting as the given matrix on the two sites of an edge and as the identity elsewhere.
3. The spectrum is taken as the set of **real** numbers in the matrix spectrum, and $\lambda_0$ is its infimum; every statement carries the Hermiticity hypotheses that make this the usual spectrum. Multiplicities are dimensions of eigenspaces, which is how the "identity of spectra as multisets" of Theorem 9 is expressed.
4. Gapped, gapless and the energy density are properties of the whole family $\{H^{\Lambda(L)}\}_L$ generated by a fixed triple of matrices, exactly as in Definitions 1 and 2.
5. Operator norms are $\ell_2$ operator norms; the local interaction strength is the maximum of the three.
6. Machines are represented by partial recursive codes: "halts on input $n$" is definedness of the evaluation, and "has not halted after $L$ steps" is the step-bounded evaluation returning nothing. The explicit local-dimension bounds of Lemma 8 and Theorem 9, which are stated in the source in terms of the number of internal states and the alphabet size of a Turing machine, are replaced by the existence of a finite local dimension.
Degenerate readings are excluded: a zero local dimension satisfies none of the statements, since a non-degenerate ground state requires a one-dimensional eigenspace and the gapless condition requires a non-empty spectrum; and every existential statement fixes the matrices before quantifying over all instances $n$ and all lattice sizes $L$.
Contributions are welcome at any milestone, and also on the infrastructure the milestones need — Wang tilings and the Robinson tile set, Gottesman–Irani history-state Hamiltonians, and quantum Turing machines in the Bernstein–Vazirani sense — which are needed for Theorem 6 and Lemma 47 of the source and are not yet part of this mission's item list.
## Selected references
- T. S. Cubitt, D. Pérez-García, M. M. Wolf, *Undecidability of the Spectral Gap* (full version), Forum of Mathematics, Pi 10:e14, 1–102 (2022). https://doi.org/10.1017/fmp.2021.15 — the version all statements of this mission are formalized against; preprint: https://arxiv.org/abs/1502.04573
- T. S. Cubitt, D. Pérez-García, M. M. Wolf, *Undecidability of the spectral gap*, Nature 528, 207–211 (2015). https://doi.org/10.1038/nature16059
- R. M. Robinson, *Undecidability and nonperiodicity for tilings of the plane*, Inventiones Mathematicae 12, 177–209 (1971). https://doi.org/10.1007/BF01418780
- D. Gottesman, S. Irani, *The quantum and classical complexity of translationally invariant tiling and Hamiltonian problems*, FOCS 2009. https://arxiv.org/abs/0905.2419
- E. Bernstein, U. Vazirani, *Quantum complexity theory*, SIAM J. Comput. 26, 1411–1473 (1997). https://doi.org/10.1137/S0097539796300921
- J. Bausch, T. S. Cubitt, A. Lucia, D. Pérez-García, *Undecidability of the spectral gap in one dimension*, Phys. Rev. X 10, 031038 (2020). https://doi.org/10.1103/PhysRevX.10.031038
Ngo's Fundamental Lemma II: Isogenies of Root Data and Paired GroupsResearch Paper
## Motivation
Waldspurger's **non-standard fundamental lemma** is an identity between stable orbital
integrals on the Lie algebras of two reductive groups that are not isomorphic, and not even
isogenous as algebraic groups, but whose root data become identified after tensoring with
$\mathbb{Q}$. The basic example is the pair $(\mathrm{Sp}_{2n}, \mathrm{SO}_{2n+1})$, whose
root systems $C_n$ and $B_n$ are exchanged by Langlands duality; the identity is what allows
the *twisted* fundamental lemma to be deduced from the ordinary one. Waldspurger formulated
the conjecture in *L'endoscopie tordue n'est pas si tordue* (2008); it is Theorem 1.12.7 of
Bao Chau Ngo, *Le lemme fondamental pour les algebres de Lie*, Publ. Math. IHES **111** (2010),
1-169 ([DOI](https://doi.org/10.1007/s10240-010-0026-7)), proved there in equal characteristic
by the same Hitchin-fibration argument that gives the ordinary fundamental lemma.
Before any of that geometry can start, the two sides have to be compared: one needs a single
Cartan subalgebra, a single Weyl group and a single space of characteristic polynomials serving
both groups at once. Producing that comparison is a self-contained piece of linear algebra over
the root data, carried out in Ngo's §1.12, and it is what this mission asks for.
## Setting
Let $G_1$ and $G_2$ be split reductive groups over a field, pinned, with maximal tori $T_1$ and
$T_2$. Each is determined by its **root datum**
$(X^*(T_i), X_*(T_i), \Phi_i, \Phi_i^\vee, \Delta_i)$, where $\Phi_i$ is the set of roots,
$\Phi_i^\vee$ the set of coroots and $\Delta_i$ the set of simple roots singled out by the
pinning.
An **isogeny of root data** between $G_1$ and $G_2$ (Ngo, Definition 1.12.1) is a pair of
isomorphisms of $\mathbb{Q}$-vector spaces
$$ \psi^* : X^*(T_2)\otimes\mathbb{Q} \longrightarrow X^*(T_1)\otimes\mathbb{Q}, \qquad
\psi_* : X_*(T_1)\otimes\mathbb{Q} \longrightarrow X_*(T_2)\otimes\mathbb{Q} $$
which are transposes of one another, such that $\psi^*$ carries the set of lines
$\mathbb{Q}\alpha_2$ ($\alpha_2 \in \Phi_2$) bijectively onto the set of lines
$\mathbb{Q}\alpha_1$ ($\alpha_1\in\Phi_1$), matching lines of simple roots with lines of simple
roots, and such that $\psi_*$ has the same property for the lines spanned by coroots. Two
semisimple groups with the same adjoint group are isogenous in this sense; so are a group and
its Langlands dual, the interesting cases being $B_n \leftrightarrow C_n$, $F_4$ and $G_2$,
where a short root $\alpha$ is sent to $\check\alpha$ and a long root to $n\check\alpha$ with
$n = |\alpha_{\mathrm{long}}|^2/|\alpha_{\mathrm{short}}|^2$. Groups obtained by twisting a
pair of isogenous pinned groups by a common torsor are called **paired**.
A prime $p$ is **good with respect to $\psi^*$** when it divides neither of the indices
$$ \bigl|X_*(T_1)/(X_*(T_1)\cap X_*(T_2))\bigr| \quad\text{and}\quad
\bigl|X_*(T_2)/(X_*(T_1)\cap X_*(T_2))\bigr|, $$
the two lattices being compared inside the single $\mathbb{Q}$-vector space identified by
$\psi_*$.
## Formalization targets
### Goal (1.12.4 and 1.12.6): the Weyl groups are identified compatibly
$$ \psi_* \, w \, \psi_*^{-1} \in W_2 \quad \text{for all } w \in W_1,
\qquad\text{and conversely,} $$
i.e. conjugation by $\psi_*$ carries the Weyl group $W_1$ acting on
$X_*(T_1)\otimes\mathbb{Q}$ onto the Weyl group $W_2$ acting on $X_*(T_2)\otimes\mathbb{Q}$.
Ngo's reason is that the reflection attached to a root depends only on the line through that
root, so the bijection of root lines transports reflections to reflections. This equivariance
is what makes the induced isomorphism $\mathfrak{t}_1 \to \mathfrak{t}_2$ descend to an
isomorphism $\nu : \mathfrak{c}_{G_1} \to \mathfrak{c}_{G_2}$ of the spaces of characteristic
polynomials, which is Lemme 1.12.6 and which is what allows two points $a_1$ and $a_2$ with
$\nu(a_1) = a_2$ to be compared at all.
### Milestones
Two steps lead there: the reflection computation that makes a matched pair of root lines give
a matched pair of reflections, and the integral statement behind Ngo's good-characteristic
hypothesis — that when the two indices above are invertible in the base ring, the two lattices
become identified after base change.
## Significance
Theorem 1.12.7, the non-standard fundamental lemma, asserts that for two paired groups over
$O_v = k[[\varpi]]$ with residue characteristic exceeding twice the Coxeter numbers, and for
points $a_1$ and $a_2$ corresponding under $\nu$, the stable orbital integrals of the
characteristic functions of $\mathfrak{g}_1(O_v)$ and $\mathfrak{g}_2(O_v)$ agree. Waldspurger
showed that this identity, together with the ordinary fundamental lemma, implies the twisted
fundamental lemma. None of the objects in that statement — reductive group schemes over a
discrete valuation ring, orbital integrals, Haar measures on the centralizer tori — exists in
Mathlib today. The comparison of §1.12 does not need any of them: it is a statement about
lattices, root systems and Weyl groups, and it is a strict prerequisite, since without the
isomorphism $\nu$ the two sides of Theorem 1.12.7 cannot even be matched up.
Beyond this paper, the notion of an isogeny of root data and the good-characteristic base
change of a pair of lattices are reusable: they are the standard bookkeeping behind Langlands
duality for split groups, and neither is currently available.
## Difficulty
The reflection step looks like a one-line computation and is one — but only once the two
proportionality constants are known to agree. If $\psi^*(\alpha_2) = c\,\alpha_1$ and
$\psi_*(\alpha_1^\vee) = c'\,\alpha_2^\vee$, the conjugate of $s_{\alpha_1}$ is $s_{\alpha_2}$
exactly when $c = c'$, and that is forced by transposition together with
$\langle\alpha,\alpha^\vee\rangle = 2$. The genuine difficulty in the goal is different: the
definition only says that $\psi^*$ and $\psi_*$ permute *lines*, so one has to show that the
bijection induced on root lines and the bijection induced on coroot lines are the *same*
bijection. A solver who assumes this without proof has assumed the substance of 1.12.4.
The lattice milestone has its own trap: the quotient $\Lambda_1/(\Lambda_1\cap\Lambda_2)$ must
be shown to have vanishing $\mathrm{Tor}$ after base change, not merely to vanish, or the
inclusion becomes only surjective.
## Formalization scope
Root data are modelled by Mathlib's `RootPairing ι ℚ M N`, with $M$ the character space, $N$
the cocharacter space, and rational coefficients throughout, so that "tensoring with
$\mathbb{Q}$" is built into the ambient objects rather than performed explicitly. A choice of
simple roots is recorded as a subset of the index type rather than as a `RootPairing.Base`;
nothing in the statements depends on that subset beyond its role in the definition of an
isogeny. The Weyl group is the subgroup of linear automorphisms of the cocharacter space
generated by the coreflections, which is the form in which it acts on the Cartan.
The goal is stated as a two-sided intertwining property rather than as an equality of
subgroups: every element of $W_1$ is intertwined by $\psi_*$ with some element of $W_2$ and
conversely. This avoids introducing a conjugation homomorphism, and it is the form in which
the statement is used. Both root pairings in the goal are required to be finite, reduced root
systems, matching Ngo's hypothesis that $G_1$ and $G_2$ are reductive groups.
The good-characteristic condition is formalized exactly as Ngo writes it, by the invertibility
in the base ring of the two indices, each expressed as the cardinality of an explicit quotient
group; the conclusion is the bijectivity of the map induced on the tensor product by the
inclusion of the intersection. If a quotient were infinite its cardinality is reported as $0$,
and invertibility of $0$ then forces the base ring to be trivial, so no false statement hides
in that corner.
No statement here is vacuous: any pair consisting of a root system and itself, with $\psi^*$
and $\psi_*$ the identity, satisfies every hypothesis, and the pair $(B_n, C_n)$ gives the
intended non-trivial instances.
## Selected references
- Bao Chau Ngo, *Le lemme fondamental pour les algebres de Lie*, Publ. Math. IHES 111 (2010), 1-169. https://doi.org/10.1007/s10240-010-0026-7
- J.-L. Waldspurger, *L'endoscopie tordue n'est pas si tordue*, Mem. Amer. Math. Soc. 908 (2008). https://doi.org/10.1090/memo/0908
- J.-L. Waldspurger, *Le lemme fondamental implique le transfert*, Compositio Math. 105 (1997), 153-236. https://doi.org/10.1023/A:1000103112268
- T. A. Springer, *Reductive groups*, in Automorphic Forms, Representations and L-functions, Proc. Sympos. Pure Math. 33 (1979), 3-27. https://doi.org/10.1090/pspum/033.1
Esquisse d'un Programme I: Dessins d'Enfants and the Faithfulness of the Galois ActionResearch Paper
## Motivation
In *Esquisse d'un Programme* (1984), Alexandre Grothendieck describes a discovery that reorganised his mathematical interests: a finite oriented combinatorial map drawn on a surface — a **dessin d'enfant**, a child's drawing — determines canonically a smooth projective algebraic curve together with a map to the projective line ramified only above $0$, $1$ and $\infty$, and that curve and map are defined over the field $\overline{\mathbb{Q}}$ of algebraic numbers (Esquisse, §3, pp. 14–16 of the French text). Consequently the absolute Galois group $\Gamma = \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ acts on these purely combinatorial objects; in the spherical case, where the structural map is a rational function $f(z) = P(z)/Q(z)$, the action of $\gamma \in \Gamma$ is obtained simply by applying $\gamma$ to the coefficients of $P$ and $Q$. Grothendieck states in §2 (p. 9) that the resulting outer action of $\Gamma$ on the profinite fundamental group $\hat{\pi}_{0,3}$ of $\mathbb{P}^1 \smallsetminus \{0,1,\infty\}$ is **faithful**, and in §3 that the theorem of Belyi, announced at the 1978 Helsinki congress, is what makes the dictionary between combinatorics and arithmetic exact.
Timeline of the results this mission formalizes. Belyi (1979, *On Galois extensions of a maximal cyclotomic field*, Izv. Akad. Nauk SSSR) proved that a smooth projective curve over $\mathbb{C}$ is defined over a number field if and only if it admits a map to $\mathbb{P}^1$ unramified outside $\{0,1,\infty\}$; the "only if" half is an explicit construction with polynomials over $\mathbb{Q}$. Grothendieck (1984) drew the consequence that $\Gamma$ acts on dessins and asserted faithfulness of the action on $\hat{\pi}_{0,3}$. Lenstra, in an appendix to L. Schneps (ed.), *The Grothendieck Theory of Dessins d'Enfants* (LMS Lecture Notes 200, CUP 1994), showed that the action is already faithful on the much smaller class of **plane trees**, equivalently on **Shabat polynomials**. That tree-level statement is the goal of this mission, because it is the sharpest form of faithfulness that can be stated without first building the theory of étale fundamental groups.
## Setting
Work over $\overline{\mathbb{Q}}$, realized as the algebraic closure of $\mathbb{Q}$, and write $\Gamma$ for its group of field automorphisms fixing $\mathbb{Q}$ pointwise.
A nonconstant polynomial $P$ over a field $K$ is a **Belyi polynomial** (classically a *Shabat polynomial*) when every critical value of $P$ lies in $\{0,1\}$: for every $z \in K$ with $P'(z) = 0$ one has $P(z) = 0$ or $P(z) = 1$. Over an algebraically closed field of characteristic zero this says exactly that $P$, viewed as a degree-$n$ map $\mathbb{P}^1 \to \mathbb{P}^1$, is unramified outside the fibres over $0$, $1$ and $\infty$. The associated dessin is the preimage $P^{-1}([0,1])$, a plane tree with $n$ edges whose vertices are the points above $0$ and $1$, with vertex orders equal to the multiplicities of the corresponding roots of $P$ and of $P - 1$.
Two Belyi polynomials define the same dessin exactly when they are **affinely equivalent**: $Q = P(aX + b)$ for some $a \neq 0$ and some $b$. The target coordinate is already rigidified by the normalisation of the critical values to $\{0,1\}$; only the source coordinate remains free.
The group $\Gamma$ acts coefficientwise: $P^{\gamma}$ is the polynomial obtained from $P$ by applying $\gamma$ to each coefficient. This is exactly the action described in §3 of the Esquisse. It sends Belyi polynomials to Belyi polynomials, and it descends to an action on affine equivalence classes, i.e. on dessins.
## Formalization targets
### Goal — faithfulness of the Galois action on plane trees
$$\forall\, \gamma \in \Gamma,\quad \gamma \neq 1 \ \Longrightarrow\ \exists\, P \in \overline{\mathbb{Q}}[X] \text{ a Belyi polynomial with } P \not\sim_{\mathrm{aff}} P^{\gamma}.$$
Equivalently: no nontrivial element of the absolute Galois group fixes every plane tree. This is the weakest stable form of the faithfulness assertion in the Esquisse: it fixes no degree, no genus and no tree, asserting only that some dessin is moved.
### Supporting targets
- **Belyi's theorem, polynomial form.** For every finite set $S \subseteq \overline{\mathbb{Q}}$ there is a Belyi polynomial $f \in \mathbb{Q}[X]$ with $f(S) \subseteq \{0,1\}$.
- **Descent to $\overline{\mathbb{Q}}$.** Every Belyi polynomial over $\mathbb{C}$ is affinely equivalent to one whose coefficients are algebraic over $\mathbb{Q}$.
- **Galois equivariance and invariants.** $P^{\gamma}$ is again a Belyi polynomial of the same degree, and the multiplicity of $z$ as a root of $P - c$ equals the multiplicity of $\gamma(z)$ as a root of $P^{\gamma} - \gamma(c)$: the dessin's vertex and face orders are Galois invariants.
- **Finiteness of the orbit.** The set of Galois conjugates of a fixed polynomial over $\overline{\mathbb{Q}}$ is finite — the "visibly finite number of conjugates" of §3.
- **Finiteness in a fixed degree.** For each $n$ there are only finitely many monic Belyi polynomials of degree $n$ over $\overline{\mathbb{Q}}$ with vanishing subleading coefficient.
- **Separation.** For every $\alpha \in \overline{\mathbb{Q}}$ there is a Belyi polynomial $P$ such that every $\gamma$ fixing the class of $P$ fixes $\alpha$. The goal follows from this by taking $\alpha$ with $\gamma(\alpha) \neq \alpha$.
## Significance
The result itself. Faithfulness turns the combinatorics of finite maps into a faithful representation of $\Gamma$: every nontrivial automorphism of $\overline{\mathbb{Q}}$ is detected by a finite tree, so invariants of dessins (degree, valency lists, monodromy group, field of moduli) are in principle a complete set of tools for distinguishing Galois elements. It is also the entry point to the anabelian programme described in §3 of the Esquisse, since the same statement expresses that $\Gamma$ embeds into the outer automorphism group of $\hat{\pi}_{0,3}$.
Formalizing it. Belyi's theorem and the faithfulness of the Galois action on trees are both established results. Mathlib at the environment revision of this mission contains no declaration mentioning Belyi maps or dessins d'enfants, and no étale fundamental group, so both statements have to be built from the polynomial and Galois-theoretic libraries. What this mission produces is a formal version of the combinatorial half of the dictionary, in a form that avoids scheme theory entirely: everything is phrased with polynomials over $\overline{\mathbb{Q}}$ and $\mathbb{C}$, so the development rests only on Mathlib's existing polynomial, field theory and Galois theory libraries.
## Difficulty
The naive attack on the goal — exhibit one tree and one Galois element moving it — does not scale: the statement quantifies over all $\gamma \neq 1$, and $\Gamma$ has no accessible presentation. The real work is the separation statement, which demands, for an arbitrary algebraic number $\alpha$, a tree whose isomorphism class remembers $\alpha$; the construction must control both the existence of a Belyi polynomial with prescribed arithmetic and the rigidity that makes affine equivalence classes finite. Belyi's theorem in polynomial form is itself an induction on the degree of the field of definition of the critical values, and each step changes the polynomial, so bookkeeping of critical values through composition is the bulk of the formal proof. The descent statement over $\mathbb{C}$ is not a formal manipulation either: it needs the finiteness of the set of Belyi polynomials of a given degree up to affine equivalence, which is where the combinatorial classification enters.
## Formalization scope
Conventions fixed in the Lean development, and not to be re-litigated by solvers:
- $\overline{\mathbb{Q}}$ is `AlgebraicClosure ℚ`, and $\Gamma$ is its group of $\mathbb{Q}$-algebra automorphisms.
- "Belyi polynomial" means: positive degree, and every root of the formal derivative is sent to $0$ or $1$. Critical values are required to lie *in* $\{0,1\}$, not to be exactly $\{0,1\}$; degenerate cases such as $X^n$ (one finite critical value) are therefore included.
- Being a Belyi polynomial is stated over an arbitrary field but is only intended over algebraically closed fields ($\overline{\mathbb{Q}}$, $\mathbb{C}$), where quantifying over the field's own elements captures all critical points.
- Dessin isomorphism is modelled as affine equivalence of the source variable only; conjugating by an affine map of the target is excluded, since the target is rigidified by $\{0,1\}$.
- The Galois action is coefficientwise application of $\gamma$.
Trivialization is ruled out as follows: the goal asserts the *existence* of a moved Belyi polynomial for each nontrivial $\gamma$, with the nondegeneracy `0 < deg P` built into the definition, so no constant or empty witness satisfies it, and no hypothesis of the goal is vacuous ($\gamma \neq 1$ is satisfiable).
A complete development needs: critical values and their behaviour under composition of polynomials; the classification of Belyi polynomials of fixed degree up to affine equivalence; Galois descent for a finite set of polynomials stable under conjugation; and, for the descent target, the identification of the coefficients of a Belyi polynomial over $\mathbb{C}$ as algebraic numbers. All of these are reusable outside this mission. Contributions of general polynomial-ramification infrastructure are welcome, as are alternative formalizations of the same statements over a general algebraically closed field of characteristic zero.
## Selected references
- A. Grothendieck, *Esquisse d'un Programme* (1984), published in L. Schneps and P. Lochak (eds.), *Geometric Galois Actions 1*, LMS Lecture Note Series 242, Cambridge University Press, 1997. https://doi.org/10.1017/CBO9780511758874
- G. V. Belyi, *On Galois extensions of a maximal cyclotomic field*, Izv. Akad. Nauk SSSR Ser. Mat. 43 (1979), 267–276. English translation: Math. USSR-Izv. 14 (1980), 247–256. https://doi.org/10.1070/IM1980v014n02ABEH001096
- L. Schneps (ed.), *The Grothendieck Theory of Dessins d'Enfants*, LMS Lecture Note Series 200, Cambridge University Press, 1994. https://doi.org/10.1017/CBO9780511569302
- S. K. Lando and A. K. Zvonkin, *Graphs on Surfaces and Their Applications*, Encyclopaedia of Mathematical Sciences 141, Springer, 2004. https://doi.org/10.1007/978-3-540-38361-1