All missions

Motivation

Existence of equilibrium is the first question any model of strategic interaction must answer, and the classical answer — Nash's theorem via Kakutani's fixed point theorem — asks for a convex, compact strategy space and continuous payoffs. Many of the models economists actually use do not have that: a firm's technology set can be discrete or irregular, and a payoff need only be upper semicontinuous, not continuous. Topkis [1979] showed that when a game's structure is instead order-theoretic — each player's strategies form a lattice, and the players' incentives reinforce each other in a precise sense — an equilibrium exists without any convexity or continuity assumption at all, and the proof method delivers something Kakutani's theorem cannot: a greatest and a least equilibrium point, with the whole equilibrium set forming a complete lattice. Zhou [1994] later showed the completeness of the equilibrium lattice in full generality; this mission formalizes the resulting theorem (Topkis's Theorem 4.2.1) together with its parametric extension (Theorem 4.2.2, established independently by Milgrom and Roberts [1990a] and Sobel [1988]), which shows how the greatest and least equilibria move as a parameter of the game — its technology, its cost structure — changes. This machinery underlies monotone comparative statics for games throughout economics: oligopoly models with strategic complements, coordination games, and search and matching models with increasing returns.

Setting

A noncooperative game $(N, S, \{f_i : i \in N\})$ consists of a finite player set $N$, a set $S \subseteq \mathbb{R}^m$ of feasible joint strategies $x = (x_i)_{i \in N}$ (allowing the set of strategies feasible for one player to depend on the others' choices, so $S$ need not be a product set), and a payoff function $f_i$ for each player $i$. Write $x_{-i}$ for the strategies of every player but $i$, $S_i(x_{-i})$ for the section of $S$ at $x_{-i}$ — player $i$'s feasible strategies given the others' choice — and $Y_i(x_{-i}) = \operatorname{argmax}_{y_i \in S_i(x_{-i})} f_i(y_i, x_{-i})$ for player $i$'s best-response set. The best joint response correspondence is $Y(x) = \prod_{i \in N} Y_i(x_{-i})$. A feasible $x'$ is an equilibrium point if $f_i(y_i, x'_{-i}) \le f_i(x')$ for every player $i$ and every feasible deviation $y_i \in S_i(x'_{-i})$ — no player can unilaterally improve.

A lattice is a partially ordered set in which every pair of elements has a join $\vee$ and a meet $\wedge$. A function $g$ is supermodular on a subset if $g(x) + g(y) \le g(x \vee y) + g(x \wedge y)$ for all $x, y$ in it, and has increasing differences in two of its arguments $(y,t)$ if $y \mapsto g(y, t'') - g(y, t')$ is monotone whenever $t' \prec t''$. A game $(N, S, \{f_i\})$ is a supermodular game if $S$ is a sublattice, $f_i(y_i, x_{-i})$ is supermodular in $y_i$ for every fixed $x_{-i}$ and every $i$, and $f_i(y_i, x_{-i})$ has increasing differences in $(y_i, x_{-i})$ for every $i$ — jointly, the conditions under which each player's own strategy components are complements and complementary to the other players' strategies (Theorem 2.6.1 of chunk 01-lattices/02-monotonicity's book).

Formalization targets

Goal — Theorem 4.2.1

If $(N, S, \{f_i\})$ is a supermodular game, $S$ is nonempty and compact, and each $f_i(y_i, x_{-i})$ is upper semicontinuous in $y_i$ on $S_i(x_{-i})$ for every $x_{-i}$ and every $i$, then

$$\{\text{equilibrium points of } (N, S, \{f_i\})\}$$

is nonempty, has a greatest and a least element, and, under the order it inherits from $\mathbb{R}^m$, is itself a nonempty complete lattice.

Theorem 4.2.2 (the parametric extension)

Let $T$ be a partially ordered set and, for each $t \in T$, $(N, S^t, \{f_i^t\})$ a supermodular game with $S^t$ nonempty, compact, and increasing in $t$; suppose each $f_i^t(y_i, x_{-i})$ is upper semicontinuous in $y_i$ and has increasing differences in $(y_i, t)$. Then for every $t$ there exist a greatest and a least equilibrium point of game $t$, and both are increasing functions of $t$ on $T$ — the equilibrium set moves monotonically as the parameter increases.

Two supporting results are formalized as milestones because Theorem 4.2.1's own proof uses them directly: Lemma 4.2.1 (equilibrium points are exactly the fixed points of the best joint response correspondence) and Lemma 4.2.2, parts (b) and (f) (the best joint response set is a nonempty compact sublattice for every feasible $x$, and the correspondence is increasing in $x$).

Significance

The result itself. Theorem 4.2.1 is the lattice-theoretic alternative to Nash/Kakutani existence: it needs no convexity of $S$ and no continuity of $f_i$ (upper semicontinuity suffices), and in exchange it delivers a greatest and a least equilibrium — with an explicit order-theoretic characterization via Theorem 2.5.1 of chunk 01-lattices — and the guarantee that the entire equilibrium set is a complete lattice, not merely nonempty. Theorem 4.2.2 gives this existence result teeth for applied comparative statics: it says that if a firm's cost structure, a market's demand parameter, or any other feature of the game increases (in the sense of the induced set order on $S^t$ and increasing differences in the payoffs), the extremal equilibria increase too — the qualitative content behind results such as "more competition leads to lower prices" in supermodular oligopoly models.

Formalizing it. The platform's existing Nash-equilibrium theorem (AGT.nash_existence, Theorem 1.8 of Algorithmic Game Theory) is a Brouwer/Kakutani argument for finite games with mixed strategies: it needs finiteness of every player's strategy set (so that mixed strategies form a compact convex simplex) and gives no lattice structure on the equilibrium set at all. Theorem 4.2.1 is a different technique entirely — it needs no finiteness, no mixing, and no convexity, and its conclusion (a complete lattice of equilibria) is exactly the content Brouwer/Kakutani cannot give. This mission is therefore not a restatement of Nash's theorem in different notation, but a second, independent existence technique with a strictly different structural payoff, formalized here for the first time on the platform. It builds directly on chunk 01-lattices's Theorem 2.5.1 (Zhou's fixed point theorem for increasing correspondences) and chunk 02-monotonicity's supermodularity/increasing differences definitions, both formalized earlier in this series.

Difficulty

The natural first idea for existence — "the best joint response correspondence has a fixed point by some general fixed-point theorem for correspondences" — needs the correspondence to be convex-valued and upper hemicontinuous for a Kakutani argument, neither of which supermodularity or upper semicontinuity alone supply: a best-response set under only upper semicontinuity can be a disconnected, non-convex set (e.g. the maximizers of a supermodular but non-quasiconcave function). The actual route goes through order instead of topology: Lemma 4.2.2 shows the best joint response set is a compact sublattice (hence subcomplete, by Theorem 2.3.1) and that the correspondence is increasing under the induced set order, which is exactly the hypothesis Theorem 2.5.1's non-constructive supremum/infimum construction needs — no convexity anywhere. A second subtlety, which the mission is careful not to elide: the equilibrium set of a supermodular game need be neither compact nor a sublattice of $\mathbb{R}^m$ when there are more than one player (Topkis's Examples 4.2.1 and 4.2.2 exhibit both failures); only the weaker claim — a complete lattice under the inherited order — is true in general, and that is what Theorem 2.5.1(b) supplies.

Formalization scope

A joint strategy is represented as a dependent function ∀ i, Fin (m i) → ℝ over a finite player type ι, with a player's own strategy accessed and overwritten via Function.update, so that $x_{-i}$ is never reified as a separate object — every statement about $f_i(y_i, x_{-i})$ or membership in $S_i(x_{-i})$ substitutes y for x's own i-th coordinate directly. IsSupermodularGame reuses chunk 02-monotonicity's SupermodularOn and IncreasingDifferencesOn verbatim, applied to each player's own payoff, rather than restating the supermodularity/increasing- differences conditions from scratch — a formalization that inlined a weaker, ad hoc notion here (e.g. supermodularity of the joint payoff vector rather than each player's own payoff in their own strategy) would trivialize the connection to chunk 02-monotonicity's theorems that the book's own proof relies on. Theorem 4.2.1's "nonempty complete lattice" conclusion is formalized, as in chunk 01-lattices, via IsLUB/IsGLB on the subtype of equilibrium points — never as membership of the ambient $\mathbb{R}^m$ supremum/infimum in the equilibrium set, which the book's own Examples 4.2.1–4.2.2 refute; a solution that instead proved the equilibrium set compact or a sublattice of $\mathbb{R}^m$ would be proving a strictly stronger and false claim. Only parts (b) and (f) of Lemma 4.2.2 are formalized, since those are the only two of its eight parts the proof of Theorem 4.2.1 uses; a complete development still needs chunk 01-lattices's Theorem 2.3.1 (subcomplete iff compact) and Theorem 2.5.1/2.5.2, and chunk 02-monotonicity's Theorem 2.8.1 and Corollary 2.7.1, none of which are restated here.

Selected references

• Topkis, D. M., Equilibrium points in nonzero-sum n-person submodular games, SIAM Journal on Control and Optimization 17(6), 1979, pp. 773–787. https://doi.org/10.1137/0317054
• Zhou, L., The set of Nash equilibria of a supermodular game is a complete lattice, Games and Economic Behavior 7(2), 1994, pp. 295–300. https://doi.org/10.1006/game.1994.1051
• Milgrom, P. and Roberts, J., Rationalizability, learning, and equilibrium in games with strategic complementarities, Econometrica 58(6), 1990, pp. 1255–1277. https://doi.org/10.2307/2938316
• Sobel, M. J., Isotone comparative statics for supermodular games, unpublished manuscript, 1988 (cited by Topkis [2011], Theorem 4.2.2).
• Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 4, §4.1–4.2.

Motivation

Online convex optimization (OCO) models a repeated decision process: at each round a learner picks a point in a convex set, an adversary (or the world) reveals a convex cost function, the learner pays that cost at its own point, and the process repeats. No statistical assumption on the sequence of costs is made. This model, introduced by Zinkevich [Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003], underlies most of modern online learning: portfolio selection, online routing, and — through its special case of stochastic optimization — the training of essentially every large machine-learning model in current use, since stochastic gradient descent (the subject of §3.4 of this chapter) is exactly an application of the regret bounds proved here.

The algorithm this chapter introduces, online gradient descent (OGD), is the field's default answer: take a gradient step against the most recently observed cost, project back onto the feasible set. It predates OCO itself as a heuristic, but Zinkevich's contribution — and this chapter's — is the regret analysis: a guarantee that holds against every sequence of costs, adversarially chosen, with an explicit, small constant. Precursors for less general settings appear in Kivinen and Warmuth [1997]; logarithmic-regret algorithms for OCO, the subject of §3.3 here, are due to Hazan, Agarwal and Kale [2007].

The online convex optimization protocol

Fix a convex set $K$ in a real inner product space, playing the role of the decision (or "action") space, and a sequence of cost functions $f_1, f_2, \dots : K \to \mathbb{R}$, each convex. At round $t$, the learner (not knowing $f_t$) plays a point $x_t \in K$, then observes $f_t$ and pays $f_t(x_t)$. Regret after $T$ rounds compares the learner's cumulative cost to that of the single best fixed decision made with hindsight of the whole sequence:

$$\mathrm{Regret}_T = \sum_{t=1}^{T} f_t(x_t) - \min_{x^\star \in K} \sum_{t=1}^{T} f_t(x^\star).$$

A learner with regret $o(T)$ is, on average, eventually as good as the best fixed point in $K$, even though it never knew the cost sequence in advance.

Two chapter-wide parameters bound how hard an instance can be: $D$, the diameter of $K$ ($\operatorname{dist}(x,y) \le D$ for all $x, y \in K$), and $G$, a common bound on the gradient norm of every $f_t$ over $K$ ($\|\nabla f_t(x)\| \le G$ for all $x \in K$), which implies but is strictly stronger than $G$-Lipschitzness on $K$. Online gradient descent (Algorithm 8) plays $x_1 \in K$ arbitrarily, then at every round sets $y_{t+1} = x_t - \eta_t \nabla f_t(x_t)$ and projects, $x_{t+1} = \Pi_K(y_{t+1})$, for a sequence of step sizes $\eta_t$ chosen in advance.

Formalization targets

Goal: Theorem 3.1 (online gradient descent regret)

$$\mathrm{Regret}_T \le \frac{3}{2} G D \sqrt{T} \quad \text{for all } T \ge 1,$$

using step sizes $\eta_t = D / (G\sqrt{t})$. This is the chapter's — and arguably the book's — central result: the simplest algorithm for the fully general OCO protocol already attains $O(\sqrt{T})$ regret, with an explicit small constant, against convex Lipschitz costs with no further structure.

Milestone: Theorem 3.2 (matching lower bound)

Any algorithm for OCO incurs $\Omega(DG\sqrt{T})$ regret in the worst case: no algorithm, however clever, can improve asymptotically on Theorem 3.1's rate. This is the weaker, worst-case-existence half of the theorem (see Formalization scope).

Milestone: Theorem 3.3 (logarithmic regret under strong convexity)

If every $f_t$ is additionally $\alpha$-strongly convex, the same algorithm — with only the step sizes changed to $\eta_t = 1/(\alpha t)$ — achieves

$$\mathrm{Regret}_T \le \frac{G^2}{2\alpha}(1 + \log T).$$

Strong convexity is a strictly stronger hypothesis than convexity, so this target does not subsume the goal; it sits alongside it as the chapter's second, sharper regime.

Significance

Theorem 3.1 is the reference point against which every later algorithm and every later chapter's improvement (Online Newton Step, RFTL, adaptive-regret methods) is measured: any new algorithm for OCO is judged first by whether it matches this $O(\sqrt{T})$ rate, then by what extra structure lets it do better. Theorem 3.2 closes the question for the general convex-Lipschitz class: $O(\sqrt{T})$ is not an artifact of a loose analysis, it is information-theoretically necessary. Theorem 3.3 identifies the one extra hypothesis (strong convexity) that buys an exponential improvement in the horizon dependence, from $\sqrt{T}$ to $\log T$, without any other change to the algorithm — the same phenomenon that in the book's Chapter 2 separated well-conditioned from general convex offline optimization, now transplanted to the online, adversarial setting.

None of these three statements has a machine-checked proof on the platform prior to this mission (see Formalization scope below for what was checked). Formalizing them establishes the regret protocol and the OGD algorithm as reusable definitions for the rest of this thirteen-chapter series, several chapters of which (Online Newton Step, RFTL, bandit convex optimization) build directly on Algorithm 8 or its regret guarantee.

Difficulty

The regret bound's proof (Theorem 3.1) is short but not naive: bounding $\nabla_t^\top(x_t - x^\star)$ by convexity alone gives no telescoping structure, so the argument instead bounds it using the projection step — the Pythagorean inequality $\|\Pi_K(z) - x^\star\| \le \|z - x^\star\|$ for $x^\star \in K$ — applied to the specific point $z = x_t - \eta_t \nabla_t$. This turns the per-round convexity bound into a telescoping sum in $\|x_t - x^\star\|^2$, and only the resulting sum, evaluated with the specific step-size schedule $\eta_t = D/(G\sqrt{t})$, produces the $\sqrt{T}$ rate; a constant or linearly growing step size does not. The same projection argument is reused for Theorem 3.3, where the strong-convexity inequality is engineered to make the $\|x^\star - x_t\|^2$ terms cancel exactly against the projection telescoping, leaving a harmonic sum. Theorem 3.2's difficulty is of a different kind: it is a lower bound over every algorithm, proved by exhibiting a randomized hard instance (the hypercube with $2^n$ sign-vector linear costs) on which no algorithm can do better than random guessing in expectation.

Formalization scope

$K$ is formalized as a subset of an arbitrary real, complete inner product space (not fixed to $\mathbb{R}^n$), since the chapter's argument uses only Hilbert-space structure. Rounds are 0-indexed (Finset.range T) rather than the book's 1-indexed rounds, so a step size stated here at round $t$ is the book's step size at round $t+1$. D and G are carried as shared section hypotheses (the chapter-wide diameter and gradient-norm bounds), not re-derived or re-stated per theorem; G is formalized exactly as the book defines it (p. 20: a bound on $\|\nabla f_t(x)\|$ over $K$, via Mathlib's HasGradientAt), not as the weaker two-point Lipschitz condition it implies — an earlier draft used the weaker Lipschitz hypothesis and was corrected during moderation, since it made the drafted theorems strictly stronger than the book's own (true by an added argument the book does not give, but not faithful to the stated proof). The projection step is formalized relationally (IsMetricProjection, an arbitrary closest point) rather than as a canonical function, since a general convex set need not come with one built into Mathlib.

For Theorem 3.2, this mission formalizes the theorem's main sentence — the worst-case existence claim — quantifying over "any algorithm" as a non-anticipating map from the full cost sequence to the play sequence, with the hard cost sequence existentially quantified after the algorithm and the horizon: for every algorithm and every horizon there is a cost sequence forcing $\Omega(DG\sqrt{T})$ regret against it. (An earlier draft quantified the cost sequence first — one fixed sequence defeating every algorithm — which is false: a constant algorithm playing a minimizer of that one sequence has zero regret against it; this was corrected during moderation.) It does not formalize the theorem's parenthetical strengthening, that the same $\Omega(DG\sqrt{T})$ bound holds even when costs are drawn from a fixed stationary distribution; that claim is about expected regret of a deterministic algorithm against a random cost sequence, and would need a probability-space formalization of the OCO protocol that this mission's definitions do not build. A formalization limited to the deterministic worst case does not trivialize the theorem: it is exactly the inequality "$O(\sqrt{T})$ cannot be improved," stated without the randomization machinery of its proof.

Theorem 3.4 (the stochastic gradient descent corollary, via a noisy gradient oracle with bounded second moment) is not included: it needs an expectation over a random oracle applied at a random, round-dependent point, which is a substantially heavier probabilistic object than the deterministic protocol built here, and is left for a future mission or an extension of this one.

Selected references

• Zinkevich, M. Online Convex Programming and Generalized Infinitesimal Gradient Ascent. ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
• Kivinen, J. and Warmuth, M. K. Exponentiated Gradient Versus Gradient Descent for Linear Predictors. Information and Computation, 1997. https://doi.org/10.1006/inco.1996.2612
• Hazan, E., Agarwal, A. and Kale, S. Logarithmic Regret Algorithms for Online Convex Optimization. Machine Learning 69, 2007. https://doi.org/10.1007/s10994-007-5016-8
• Hazan, E. Introduction to Online Convex Optimization, 2nd ed. arXiv:1909.05207v3, Chapter 3. https://arxiv.org/abs/1909.05207

Motivation

Consider a decision maker who must choose, at each of $T$ rounds, between two actions on the advice of $N$ "experts," none of which is known in advance to be reliable. This is the prediction-from-expert-advice problem, introduced by Littlestone and Warmuth [Littlestone & Warmuth, The Weighted Majority Algorithm, FOCS 1989/Inf. Comput. 1994] and generalized to real-valued losses by Freund and Schapire's Hedge algorithm [Freund & Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, JCSS 1997]. It is one of the two founding problems of online learning (the other being universal portfolio selection, also introduced in this book's first chapter) and the historical origin of the multiplicative-weights update method, later recognized as a single algorithmic idea underlying results across game theory, optimization, and computational complexity [Arora, Hazan & Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 2012]. This mission formalizes the chapter's three central guarantees: a matching deterministic lower bound, the Weighted Majority mistake bound, and Hedge's loss bound — the earliest instance, in the book's own development, of the "online convex optimization" phenomenon that its later chapters generalize to arbitrary convex losses.

Setting

At each round $t = 1, \dots, T$, a decision maker chooses one of two actions, $A$ or $B$. After the choice, the true outcome for that round is revealed, and any action that disagrees with it is charged a mistake. $N$ experts also each commit to a prediction every round, and the decision maker may consult their record.

The Weighted Majority (WM) algorithm maintains a weight $W_t(i)$ for each expert $i$, initialized to $W_1(i) = 1$. It predicts whichever action currently carries at least half the total weight, and after seeing the outcome, multiplies the weight of every expert who erred by $(1-\varepsilon)$ for a fixed parameter $\varepsilon \in (0, 1/2)$, leaving correct experts' weights unchanged. $M_T$ denotes the algorithm's own mistake count through round $T$, and $M_T(i)$ expert $i$'s.

The Randomized Weighted Majority (RWM) algorithm uses the same weights, but instead of following the majority it samples an expert with probability proportional to its weight, $p_t(i) = W_t(i) / \sum_j W_t(j)$, and follows that expert's prediction; $\mathbb E[M_T]$ is its expected mistake count.

Hedge generalizes further, from binary mistakes to arbitrary non-negative real-valued losses $\ell_t(i) \ge 0$ suffered by expert $i$ at round $t$. It samples expert $i_t$ with probability $x_t(i) = W_t(i)/\sum_j W_t(j)$ from weights updated multiplicatively in the loss, $W_{t+1}(i) = W_t(i) \, e^{-\varepsilon \ell_t(i)}$. Writing losses and the mixed strategy as vectors, the algorithm's expected loss at round $t$ is $x_t^\top \ell_t$.

Formalization targets

Goal — Theorem 1.5 (Hedge's loss bound)

$$\sum_{t=1}^T x_t^\top \ell_t \;\le\; \sum_{t=1}^T \ell_t(i^\star) \;+\; \varepsilon \sum_{t=1}^T x_t^\top \ell_t^2 \;+\; \frac{\log N}{\varepsilon}, \qquad \forall\, i^\star \in [N],$$

where $\ell_t^2(i) := \ell_t(i)^2$. This is the chapter's most general result and the one the book reuses later on; it leaves $\varepsilon$ free (no asymptotic tuning), so it survives whatever later chapters do with $\varepsilon$.

Milestones

• Theorem 1.1 (deterministic lower bound). With $L \le T/2$ the best expert's mistake count, no deterministic algorithm can guarantee fewer than $2L$ mistakes on every instance.
• Lemma 1.3 (Weighted Majority): $M_T \le 2(1+\varepsilon) M_T(i) + 2\log N/\varepsilon$ for every expert $i$.
• Lemma 1.4 (Randomized Weighted Majority): $\mathbb E[M_T] \le (1+\varepsilon) M_T(i) + \log N /\varepsilon$ for every expert $i$.

Significance

Theorem 1.1 shows the mistake-bound question has no trivial answer: even against only two maximally simple experts, any deterministic strategy is beaten by a factor of $2$ by an adversary who knows its code. Lemmas 1.3 and 1.4 show this factor is essentially removable — first by relaxing "guarantee" to "guarantee in expectation" (RWM halves the deterministic penalty from $2(1+\varepsilon)$ to $(1+\varepsilon)$), then Theorem 1.5 removes the binary-mistake restriction altogether, replacing it with an explicit second-moment correction term $\varepsilon \sum_t x_t^\top \ell_t^2$ that vanishes as losses shrink. Together they trace the chapter's own narrative arc from "no algorithm beats $2L$" to "an explicit, parameter-free family of algorithms gets within $(1+\varepsilon)$ of the best expert for any $\varepsilon$." All four results are proved by the book via the same device — a potential function $\Phi_t = \sum_i W_t(i)$ — one of the first instances of the potential-function method that recurs throughout the rest of the book (e.g. Online Gradient Descent's regret proof) and throughout online learning generally. None of these four statements, in this exact form, has a formalized proof on Prove2Me or (to the extent searchable) elsewhere: the platform's closest existing result, BanditAlgorithm.ftrl_simplex_exp_weights_regret (see Formalization scope below), proves an asymptotically similar bound by an entirely different route and under a different loss model.

Difficulty

The natural first attempt at any of these bounds is to track $M_T$ (or $\mathbb E[M_T]$, or $\sum_t x_t^\top \ell_t$) directly and induct on $T$; this fails because the quantity itself has no useful recursive structure — knowing the algorithm's mistake count through round $t$ says nothing about round $t+1$'s outcome, which the adversary chooses to inflict maximum damage. The proofs instead introduce an auxiliary potential $\Phi_t = \sum_i W_t(i)$ that is not the quantity being bounded, track it in two directions — an upper bound in terms of the algorithm's own performance (using $1+x \le e^x$, or, for Hedge, $e^{-x} \le 1-x+x^2$ for $x \ge 0$) and a lower bound via the single best expert's weight, $W_T(i^\star) \le \Phi_T$ — and only convert back to the mistake/loss bound at the very end via one logarithm. Getting the direction of every inequality right (each of the four proofs chains four or five inequalities, each valid only in the stated parameter range) is the entire difficulty; there is no shortcut that avoids introducing $\Phi_t$.

Formalization scope

Each algorithm is represented as a Prop-valued run predicate parametrizing over the weight sequence, the input (expert predictions/losses and true outcomes), and the algorithm's own output (predictions or mixed strategy), rather than as an executable program: IsHedgeRun fixes W 0 i = 1, the update W (t+1) i = W t i * exp(-ε * ℓ t i), and x t i = W t i / ∑ j, W t j; IsWeightedMajorityRun additionally fixes the majority-vote prediction rule explicitly (per the triage rubric, the algorithm is part of the audited statement here, not a black box the proof is free to instantiate). Randomization in RWM and Hedge is captured exactly as the book itself does — as a deterministic expectation, i.e. the inner product of the probability vector with the {0,1}-mistake or loss vector — rather than as a measure-theoretic random variable; the book's own Section 1.3.3 makes this identification explicit ("denote in vector notation the expected loss of the algorithm by $\mathbb E[\ell_t(i_t)] = x_t^\top \ell_t$"), so no probability space is introduced. Theorem 1.1's "deterministic algorithm" is a causal map from an outcome history to a prediction (prediction at round $t$ depends only on outcomes before $t$), instantiated at the book's own two-expert construction (one expert always predicts $A$, the other always $B$) rather than a fully general $N$-expert adversary argument — a strictly weaker instance of the general claim, but the exact one the book's proof establishes, so no scope is lost relative to what is proved. $\varepsilon$ is kept as an explicit free parameter throughout, per the book's own presentation (no substitution of the corollary's optimized $\varepsilon^\star = \sqrt{\log N / M_T(i^\star)}$ into the milestone statements).

A trivializing formalization to rule out: fixing $N = 1$ (a single expert) would make Lemmas 1.3–1.5 hold vacuously with $M_T = M_T(i)$ regardless of the potential-function argument; every formal statement here quantifies over an unconstrained $N : \mathbb N$ with $N > 0$, not a hard-coded small case.

The mission needs no Mathlib infrastructure beyond finite sums, Real.log, and Real.exp; the book's own OCO protocol and regret definition (§1.1) are not needed, since this chapter's proofs work directly with mistake/loss counts (per the chunk brief). BanditAlgorithm.ftrl_simplex_exp_weights_regret (Bandit Algorithms XII, Prop. 28.7, arXiv:2003.05963 §28) proves $R_n \le \sqrt{2n\log d}$ for exponential weights on the simplex against $[0,1]$-valued losses, via an FTRL/mirror-descent instantiation — the same asymptotic phenomenon as Theorem 1.5, but a different proof technique, a different (bounded, not merely non-negative) loss assumption, and stated for simplex-comparator regret rather than the per-expert loss comparator here; it is listed as a reference/comparison point, not reused.

Selected references

• N. Littlestone, M. Warmuth, The Weighted Majority Algorithm, FOCS 1989 / Information and Computation 108(2), 1994. https://doi.org/10.1006/inco.1994.1009
• Y. Freund, R. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, Journal of Computer and System Sciences 55(1), 1997. https://doi.org/10.1006/jcss.1997.1504
• S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8(1), 2012. https://doi.org/10.4086/toc.2012.v008a006
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter
  1. https://arxiv.org/abs/1909.05207

Motivation

Reinforcement learning (RL) formalizes sequential decision-making under uncertainty: an agent repeatedly observes a state, takes an action, receives a reward, and transitions to a new state, with the goal of maximizing cumulative reward over an unknown environment. It underlies applications from game-playing agents to robotics and adaptive medical treatment. What separates RL from the bandit and contextual bandit problems of earlier chapters in this series is state: the environment carries information forward across time steps, so a good action now can pay off many steps later, and a poor exploration strategy can take exponentially long to discover it. This mission formalizes the foundational results of finite-horizon episodic RL — the Markov Decision Process (MDP) model, the Bellman-optimality principle that makes dynamic programming possible, and the analytical toolkit (the performance-difference and Bellman-residual-decomposition lemmas) used throughout the field's regret analyses — culminating in a polynomial regret guarantee for UCB-VI, the canonical optimism-based algorithm for tabular RL introduced by Azar, Osband, and Munos (Minimax Regret Bounds for Reinforcement Learning, ICML 2017, arXiv:1703.05449).

Setting

A finite-horizon episodic Markov Decision Process $M = (S, A, \{P^M_h\}_{h=1}^H, \{R^M_h\}_{h=1}^H, d_1)$ consists of a finite state space $S$, a finite action space $A$, a horizon $H$, per-layer transition kernels $P^M_h : S\times A \to \Delta(S)$ and reward distributions $R^M_h : S\times A \to \Delta(\mathbb R)$, and an initial state distribution $d_1 \in \Delta(S)$. An episode unrolls for $h=1,\dots,H$: the learner selects an action $a_h \sim \pi_h(s_h)$ under a randomized non-stationary policy $\pi = (\pi_1,\dots,\pi_H) \in \Pi^{\mathrm{rns}}$ (each $\pi_h : S \to \Delta(A)$), receives reward $r_h \sim R^M_h(s_h,a_h)$, and transitions to $s_{h+1}\sim P^M_h(s_h,a_h)$. The value of $\pi$ is $f^M(\pi) := \mathbb E^{M,\pi}[\sum_h r_h]$, and the state-action and state value functions $Q^{M,\pi}_h(s,a)$, $V^{M,\pi}_h(s)$ are the analogous reward-to-go quantities from layer $h$ onward. In the online RL problem, $M^\star$ is unknown, the learner interacts with it for $T$ episodes, and the goal is to minimize the regret $\mathrm{Reg} = \sum_{t=1}^T \big(f^{M^\star} (\pi^{M^\star}) - f^{M^\star}(\pi^t)\big)$ against the best policy $\pi^{M^\star} \in \arg\max_{\pi\in\Pi^{\mathrm{rns}}} f^{M^\star}(\pi)$.

Formalization targets

Goal — Theorem 1 (UCB-VI regret)

$$\exists\, C>0,\ \forall\, \delta\in(0,1],\quad \Pr\Big[\mathrm{Reg} \le C\cdot H\cdot S\cdot\sqrt{A\,T}\cdot\sqrt{\log(SAHT/\delta)}\Big] \ge 1-\delta,$$

for the UCB-VI algorithm run with the explicit bonus $b^t_{h,\delta}(s,a) = 2\sqrt{\log(2SAHT/\delta)/n^t_h(s,a)}$, under Assumption 6 (deterministic, known, $[0,1]$-bounded rewards). This is the weakest stable form of the guarantee: it fixes only the shape of the bound (polynomial in $S,A,H,T$, logarithmic in $1/\delta$), leaving the exact leading constant — which the book itself does not pin down on this page — outside the formal claim.

Reaching it rests on three structural facts, each formalized as a milestone in attack order:

• Proposition 25 (Bellman optimality): existence of a single deterministic policy simultaneously optimal at every state, computable by backward induction — the reason dynamic programming solves planning at all.
• Lemma 13 (Performance difference) and Lemma 14 (Bellman residual decomposition): two "credit assignment" identities decomposing a value gap (between two policies, or one policy under two models) into a sum of per-layer, on-roll-in terms.
• Lemma 15 (Error decomposition for optimistic policies): the fact that a greedy policy driven by any optimistic value estimate suffers sub-optimality controlled additively — not exponentially — by that estimate's own Bellman residuals, evaluated on-policy.

Significance

The result itself. Theorem 1 is the chapter's headline result: the first guarantee, in this development, that a learning algorithm — one that does not know the environment's transitions in advance — can achieve regret growing only polynomially in the size of the state space, the action space, and the horizon, and only as $\sqrt T$ in the number of episodes. The chapter's own "combination lock" example (Figure 8) shows this is not automatic: naive exploration strategies (such as $\varepsilon$-greedy, which suffices for ordinary bandits) incur regret exponential in the horizon on some MDPs with as few as $H+2$ states. UCB-VI's guarantee is the sample-complexity foundation on which essentially every subsequent result on tabular, linear, and general function-approximation RL in the book is built.

Formalizing it. No part of this chapter's mathematical content already has a faithful counterpart on the platform (see Difficulty, below, and Formalization scope). This mission contributes: (i) a from-scratch Lean formalization of the finite-horizon episodic MDP model and its value functions, faithful to the book's $0$/$1$-indexing and reward-distribution conventions; (ii) faithful statements (drafted with sorry, not yet proved) of Proposition 25 and Lemmas 13–15; and (iii) a faithful statement of Theorem 1 itself, including a from-scratch construction of the finite $T$-episode adaptive interaction process needed to make sense of a high-probability regret guarantee. Proving these — Proposition 25 by backward induction, Lemmas 13–15 by telescoping, and Theorem 1 by combining Lemma 15's optimism bound with a concentration argument bounding the estimation-error and martingale terms of Eqs. (5.30)–(5.33) (omitted here; see Difficulty) — is open work for solvers.

Difficulty

The obvious approach to Theorem 1 — bound the regret episode-by-episode using only the fact that $Q^t$ is close to $Q^{M^\star,\star}$ in some fixed sense — fails because $Q^t$'s error is itself random (it depends on the transitions observed so far) and compounds across $H$ layers of dynamic programming. Lemma 15 defuses the compounding: it shows the sub-optimality gap is additive in the per-layer Bellman residuals rather than multiplicative, provided $Q^t$ is optimistic. Making $Q^t$ optimistic with high probability, in turn, requires a concentration argument for the empirical transition estimates $\widehat P^t_h$ (an application of Freedman's or the Azuma–Hoeffding inequality, not included among this mission's milestones) and a union bound over all $(s,a,h,t)$ — accounting for the $SAHT$ inside the bonus's logarithm. The final regret sum further requires bounding $\sum_t \sum_h 1/\sqrt{n^t_h(s^t_h,a^t_h)}$ by a pigeonhole/potential-function argument over the visitation counts, which is where the $S\sqrt{AT}$ scaling — rather than a naive $SA\sqrt{T}$ — originates. None of this concentration or counting machinery is included in the current milestones; a solver attempting Theorem 1 needs it as prerequisite lemmas.

Formalization scope

MDP and value functions. States and actions are finite types (Fintype); layers are represented $0$-indexed throughout the Lean development (the book's layer $h$ is h - 1), with the terminal convention V _ _ H _ = 0 matching $V_{H+1}\equiv 0$. Since every value/expectation formula in this chapter uses the reward distribution $R_h(s,a)\in\Delta(\mathbb R)$ only through its mean, EpisodicMDP.R records that mean directly — equivalent, by linearity of expectation, to carrying the full distribution, and changing no theorem's content. Transition kernels and policies are represented as plain real-valued functions (S → A → ℝ-style) rather than as Mathlib's PMF, with IsPolicy/the EpisodicMDP structure's own proof fields asserting the probability-distribution properties (nonnegativity, summing to $1$) where the book requires membership in $\Pi^{\mathrm{rns}}$ or a well-formed kernel; this keeps every expectation a finite Finset.sum, needing no measure theory. The optimal value functions Qstar/Vstar are defined as literal suprema over the entire (uncountable, since $|A|\ge2$) policy type — not via a recursive shortcut — which is what rules out the trivializing formalization of Proposition 25: defining Vstar by the very recursion the proposition asserts would make the proposition a tautology, whereas here it is a genuine claim about a supremum over an enormous space of competitor policies.

UCB-VI and Theorem 1. Because $S$, $A$, $H$, and $T$ are all finite, the $T$-episode adaptive interaction (in which round $t$'s policy is a function of the realized history of the first $t-1$ episodes) is modeled as a finite probability space: the outcome type Fin T → Trajectory S A H is a Fintype, "probability" is a finite sum over it, and "with probability $\ge 1-\delta$" is a plain inequality between two real numbers — no MeasureTheory is used anywhere in this mission. The universal constant $C$ in Theorem 1 is existentially quantified (∃ C > 0, …) rather than given as a literal numeral, since its value is not pinned down by the book on this page and this mission does not carry out the (non-milestoned) concentration argument that would derive it; this is the convention adopted throughout for the book's own "$\lesssim$" notation. The empirical-transition estimator inside $Q^t_h$ is defined to be $0$ when $n^t_h(s,a)=0$ (no data yet collected for that pair) — a boundary case Eq. (5.25) does not address, resolved here by convention rather than proof.

Prior art. The platform's existing BanditAlgorithm.UCRL2Algorithm mission formalizes UCRL2 for the average-reward, infinite-horizon MDP setting with a diameter parameter, and its Bellman-optimality statement is the average-cost optimality equation — genuinely different from this chapter's finite-horizon episodic Bellman recursion, even though both go by the name "Bellman optimality." No reference item was reused; every definition and theorem in this mission is drafted from scratch. Both missions bound regret via optimism over a confidence set of models, but for different objectives (average reward vs. finite-horizon cumulative reward) and different MDP classes.

Reusable infrastructure and open contributions. EpisodicMDP, Policy, V/Q/Qstar/Vstar, and stateDist/stateExp are reusable by any future mission on finite-horizon episodic RL in this book's later chapters. Contributions welcome: proofs of the four milestone lemmas (by backward induction and telescoping, respectively); the concentration lemmas underlying Theorem 1's optimism guarantee (Eqs. (5.30)–(5.33) of the source, not milestoned here); and the final regret proof combining them.

Selected references

• Foster, D. J. and Rakhlin, A., Foundations of Reinforcement Learning and Interactive Decision Making, 2023. arXiv:2312.16730v1
• Azar, M. G., Osband, I., and Munos, R., Minimax Regret Bounds for Reinforcement Learning, ICML 2017. arXiv:1703.05449
• Jaksch, T., Ortner, R., and Auer, P., Near-optimal Regret Bounds for Reinforcement Learning, JMLR 11 (2010).

Let $m$ be an odd squarefree positive integer and let $A$ be a set of units modulo $m$ with $|A| > \frac{5}{8}\varphi(m)$. Then $A + A + A = \mathbb{Z}/m\mathbb{Z}$: every residue class, unit or not, is a sum of three elements of $A$.

This is Corollary 1.5 of Xuancheng Shao, A density version of the Vinogradov three primes theorem, Duke Math. J. 163 (2014) 489-512, arXiv:1206.6139v2. It is the local input to Shao's density version of the three primes theorem, and it is a clean finite statement in its own right.

The constant is sharp and the inequality is strict

At $m = 15$ the set $\{2, 8, 11, 13, 14\}$ has five elements, so $5\varphi(15) = 8 \cdot 5$ exactly, and $1$ is not a sum of three of its elements. The hypothesis therefore fails by nothing at all and the conclusion already fails. If $<$ is weakened to $\le$, the statement is false.

Where the proof comes from

The corollary cannot be proved by induction on sets. Passing from $m$ to a prime factor $p$ splits $A$ into fibers of different densities, and a set is the wrong object to carry through that split. The induction has to run on functions $f : \mathbb{Z}/m\mathbb{Z} \to [0,1]$, and the corollary is the case $f = 1_A$ of a weighted statement, Proposition 1.4. That is the one step from which the rest follows.

The weighted statement then splits at the primes 3 and 5. For $m$ coprime to 30 the induction runs on the prime factors, using Cauchy-Davenport-Chowla for three sets modulo a prime, and it produces the stronger bilinear conclusion $f(a)f(b) + f(b)f(c) + f(c)f(a) > \frac{5}{8}(f(a) + f(b) + f(c))$. The modulus 15 is handled separately by a linear program over the eight units. Two averaging inequalities, one symmetric and one asymmetric, are what turn a density above $5/8$ into a single good triple in both halves.

What the milestones are

The nine milestones follow Shao's own numbering: the two averaging inequalities of Section 2 (Lemmas 2.1 and 2.2), the finite check at $m = 15$ (Lemma 2.3), the three-set Cauchy-Davenport-Chowla bound, the divisor reduction that lets the proof assume $15 \mid m$, the induction away from 3 and 5 (Proposition 3.1), the modulus-15 case (Proposition 3.2), the weighted local result (Proposition 1.4), and the counting bridge that the units modulo $m$ number $\varphi(m)$.

Notes on the formalization

Every item is stated in Mathlib primitives alone, so the mission needs no definition items: IsUnit, Nat.totient, Odd, Squarefree, Finset, and Antitone. The set of units modulo $m$ is written Finset.univ.filter (fun x => IsUnit x) at each use rather than through a defined abbreviation, so a reader auditing a statement has to trust only Mathlib. That is also why open scoped Classical appears in the preamble.

The density hypothesis is written 5 * Nat.totient m < 8 * A.card, which is $|A| > \frac{5}{8}\varphi(m)$ cleared of division so the whole statement stays in $\mathbb{N}$ with no rounding.

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.

Motivation

Mirror symmetry began as an empirical observation in string theory: certain pairs $(X,Y)$ of Calabi–Yau threefolds, with no evident geometric relation, give rise to the same physical theory, and invariants that are hard to compute on $X$ (counts of holomorphic curves) turn into easy computations on $Y$ (variations of complex structure). The paper Mirror symmetry is T-duality by A. Strominger, S.-T. Yau and E. Zaslow, Nucl. Phys. B 479 (1996) 243–259, proposed the first structural explanation: $X$ should carry a fibration by special Lagrangian 3-tori, the mirror $Y$ should be obtained by replacing each fibre with its dual torus, and the mirror map should be fibrewise T-duality. This proposal is now called the SYZ conjecture, and it organises most later geometric work on mirror symmetry.

The string-theoretic argument of Sections 1–2 of the paper is heuristic and is not formalizable as stated. Section 3 is different: it is a self-contained piece of differential geometry about the moduli space of a special Lagrangian submanifold together with a flat $U(1)$ connection on it. This mission formalizes Section 3.

A short timeline of the mathematics the section rests on:

• Harvey and Lawson, Calibrated geometries (Acta Math. 148, 1982), introduced special Lagrangian submanifolds as a calibrated geometry in a Calabi–Yau manifold.
• R. McLean, Deformations of calibrated submanifolds (Duke preprint 96-01, 1996; Comm. Anal. Geom. 6 (1998) 705–747), proved that the space of deformations of a compact special Lagrangian submanifold $L$ is a smooth manifold of dimension $b_1(L)$, whose tangent space at $L$ is the space of harmonic $1$-forms on $L$. The paper cites this as its reference [7].
• SYZ (1996), Section 3, add the moduli of flat $U(1)$ connections, exhibit an $L^2$ metric $g_{ab}$ and a compatible almost complex structure $\mathcal J$ on the resulting $2b_1$-dimensional moduli space $\mathcal M$, derive the identity $\partial_a g_{bc} = \partial_b g_{ac}$ (their Eq. (3.4)), and conclude that $\mathcal M$ is Kähler. They also exhibit a natural $n$-form $\Theta$ on $\mathcal M$, holomorphic when the brane is a torus.
• N. Hitchin, The moduli space of special Lagrangian submanifolds (Ann. Scuola Norm. Sup. Pisa 25, 1997), gave a rigorous treatment in which the McLean metric is Hessian with respect to natural affine structures — the coordinate-free counterpart of Eq. (3.4).

Setting

Fix $n \ge 1$. The ambient Calabi–Yau manifold is modelled by $\mathbb C^n$, carrying

• the Riemannian metric $g(u,v) = \operatorname{Re}\langle u, v\rangle$,
• the complex structure $J u = i u$,
• the Kähler form $\omega(u,v) = \operatorname{Im}\langle u,v\rangle$, which equals $g(Ju, v)$,
• the holomorphic volume form $\Omega = dz^1 \wedge \cdots \wedge dz^n$, evaluated on $n$ vectors as the complex determinant of the matrix they span, and its imaginary part $\kappa = \operatorname{Im}\Omega$.

Here $\langle\cdot,\cdot\rangle$ is the standard Hermitian product of $\mathbb C^n$, conjugate-linear in its first argument.

The brane $L$ is an $n$-torus. It is presented by its universal cover: a map $f : \mathbb R^n \to \mathbb C^n$ that is periodic up to translation,

$$f(x + e_a) = f(x) + \lambda_a, \qquad a = 1,\dots,n,$$

for a fixed family of periods $\lambda_1,\dots,\lambda_n \in \mathbb C^n$. Such an $f$ is exactly a map of the torus $\mathbb R^n/\mathbb Z^n$ into the complex torus $\mathbb C^n/\Lambda$, and integration over $L$ is integration over the unit cube $[0,1]^n$.

Write $\partial_i f$ for the partial derivatives of $f$. The map $f$ is Lagrangian at $x$ if $\omega(\partial_i f, \partial_j f) = 0$ for all $i,j$, i.e. $f^{*}\omega = 0$; it is special Lagrangian if in addition $\kappa(\partial_1 f, \dots, \partial_n f) = 0$, i.e. $f^{*}\kappa = 0$. This is the supersymmetry condition of the paper (Section 2, conditions (ii) and (iii)). The induced metric is $g_{ij} = g(\partial_i f, \partial_j f)$, the volume density is $\sqrt{\det g}$, and the second fundamental form of a Lagrangian immersion is the totally symmetric tensor

$$h_{ijk} = \omega(\partial_i \partial_j f, \partial_k f).$$

Given a family $f_t$ of such maps, its deformation $1$-form is

$$\theta_i = \omega\!\left(\tfrac{\partial f}{\partial t}, \partial_i f\right),$$

the $1$-form obtained by contracting the velocity into the Kähler form. For an $m$-parameter family $F : \mathbb R^m \to (\mathbb R^n \to \mathbb C^n)$, $t \mapsto f_t$, one gets $m$ such forms $\theta^a$, $a = 1,\dots,m$, one per moduli direction.

The moduli data of Section 3 is a smooth $m$-parameter family $F$ of special Lagrangian tori, all with the same periods, subject to two normalizations taken from the paper: each $\theta^a(t)$ is harmonic for the induced metric $g(t)$ (closed and co-closed), and the cohomology class of each $\theta^a$ is constant along the family. The $L^2$ (McLean) metric on the moduli parameters is

$$g_{ab}(t) \;=\; \int_{L} g^{ij}\,\theta^a_i\,\theta^b_j \; \sqrt{\det g}\; d^n x .$$

The full moduli space $\mathcal M$ of the paper also records the flat $U(1)$ connection; its moduli form a torus of the same dimension, with coordinates $s^a$. On $\mathcal M$, modelled by $\mathbb R^m \times \mathbb R^m$ with coordinates $(t^a, s^a)$, the paper puts the block-diagonal metric $G = g_{ab}(dt^a dt^b + ds^a ds^b)$ and the constant almost complex structure $\mathcal J(\partial_{t^a}) = \partial_{s^a}$, $\mathcal J(\partial_{s^a}) = -\partial_{t^a}$, with fundamental $2$-form $\omega_{\mathcal M}(X,Y) = G(\mathcal J X, Y)$.

Target

The goal theorem is the conclusion of Section 3: for every such family, the fundamental $2$-form of the moduli space is closed,

$$d\,\omega_{\mathcal M} = 0,$$

and since $\mathcal J$ is constant in these coordinates it is integrable, so $(\mathcal M, G, \mathcal J)$ is Kähler.

The milestones are the numbered intermediate results of the paper, in the paper's own order:

$$\textbf{Prop. 1:}\quad \frac{d}{dt} f_t^{*}\omega = d\theta .$$ $$\textbf{Prop. 2:}\quad \frac{d}{dt} f_t^{*}\kappa = -\,d(\ast\theta), \quad\text{so}\quad \frac{d}{dt} f_t^{*}\kappa = 0 \iff d^{\dagger}\theta = 0 .$$ $$\textbf{Prop. 4:}\quad \frac{d}{dt} g_{ij} = 2\,h_{ijk}\,w^{k}\quad\text{for the flow } \dot f = J f_{*} w .$$ $$\textbf{Eq. (A.2):}\quad \partial_a \theta^b \text{ is exact.}$$ $$\textbf{Eq. (3.4):}\quad \partial_a g_{bc} = \partial_b g_{ac}.$$

$$\textbf{$\Theta$ closed:}\quad \partial_c \int_L \theta^{a_1}\wedge\cdots\wedge\theta^{a_n} = 0 .

$$$$

\textbf{Hessian} \Rightarrow \textbf{Kähler:}\quad \partial_a g_{bc} = \partial_b g_{ac} ;\Longrightarrow; d,\omega_{\mathcal M} = 0 .$$

Together, Propositions 1 and 2 are the statement that the tangent space to the moduli space consists of harmonic $1$-forms — McLean's theorem in the form the paper uses it. Eq. (3.4) is the technical heart, and the last milestone is the step from it to the goal.

Significance

The result. Section 3 supplies the only rigorous mathematics in the paper. It says that the object the physics predicts to be a Calabi–Yau manifold — the moduli space of a supersymmetric brane — does carry the first piece of that structure, a Kähler metric, and that it carries a natural $n$-form which, for toroidal branes, is a holomorphic $b_1$-form and hence a candidate for the Calabi–Yau form of the mirror. Eq. (3.4) says the McLean metric is locally the Hessian of a potential; this affine-Hessian structure of the SYZ base is the starting point of the later large-complex-structure-limit programme.

Formalizing it. The Section 3 results have rigorous published proofs (McLean for the tangent space, Hitchin for the Hessian property), but no machine-checked proof exists for any of them, and Mathlib currently has no special Lagrangian geometry, no Hodge theory, and no differential forms on manifolds. The mission therefore also produces reusable infrastructure: a workable coordinate model of calibrated submanifold geometry, the variation formulas for the induced metric and for the pullbacks of $\omega$ and $\kappa$, and the Hessian-metric criterion for a Kähler structure, which is independent of the rest and reusable wherever affine-Kähler geometry appears.

Difficulty

The obvious approach to the goal — "the metric is Hessian, so take the potential and write down the Kähler form" — is not available: the potential is not part of the data, and producing it requires the symmetry $\partial_a g_{bc} = \partial_b g_{ac}$ first. That symmetry is the hard step, and it is hard for a specific reason: differentiating $g_{bc}(t) = \int_L g^{ij}\theta^b_i\theta^c_j \sqrt{\det g}$ in the direction $t^a$ produces four terms — from $\theta^b$, from $\theta^c$, from the inverse metric $g^{ij}$, and from the volume density — and only their sum is symmetric in $(a,b)$. Two of them are killed by an integration by parts that needs both harmonicity of $\theta$ and compactness of $L$ (this is where the torus, and not a coordinate patch, is essential); one is killed because a special Lagrangian submanifold is minimal, so the mean curvature term in $\partial_a \sqrt{\det g}$ vanishes; what survives is $-2\int_L h_{ijk} w_a^i w_b^j w_c^k$, which is symmetric because $h$ is a symmetric $3$-tensor. Every one of those four cancellations has to be carried out.

Proposition 2 carries a separate difficulty: it is an identity between the variation of a determinant and a divergence, and it is false without the hypothesis that $f_t$ is special Lagrangian at the point in question — for a merely Lagrangian $f$ there is a further term proportional to the Lagrangian angle.

Formalization scope

The formalization commits to the following, all of which are visible in the definition item and none of which are silent:

• The ambient Calabi–Yau is flat. Sections 2 and 3 of the paper work with a general Calabi–Yau; here the ambient space is $\mathbb C^n$ (equivalently, after imposing periodicity, a flat complex torus $\mathbb C^n/\Lambda$). This is the semi-flat/large-complex-structure regime in which the paper's own Section 2 check is carried out, and it is the price of Mathlib having no differential forms on manifolds. Propositions 1, 2 and 4 are stated for arbitrary smooth maps $\mathbb R^n \to \mathbb C^n$ and are genuinely local, so for them the restriction only removes the ambient curvature terms that the paper also drops by working in normal coordinates. The moduli-level statements do use the flat ambient.
• The brane is a torus, presented by periodicity up to a fixed period lattice; $L^2$ pairings are integrals over $[0,1]^n$ against Lebesgue measure. Compactness is used, and cannot be dropped.
• Derivatives are Fréchet derivatives of maps on $\mathbb R^k$ contracted with a standard basis vector. Lean's fderiv returns $0$ at a point of non-differentiability, so a statement about derivatives of a non-smooth map is a statement about zeros; every item therefore carries an explicit smoothness hypothesis, and the moduli-level items carry it inside the family structure.
• Matrix inversion and square roots are total. The inverse of a singular matrix is $0$ and the square root of a negative real is $0$ in Lean. The items that use $g^{ij}$ or $\sqrt{\det g}$ therefore carry an explicit immersion hypothesis $\det g \ne 0$.
• Closedness of a $2$-form is the Palais formula on constant vector fields, $d\omega(X,Y,Z) = X\,\omega(Y,Z) + Y\,\omega(Z,X) + Z\,\omega(X,Y)$, which is the exterior derivative because the fields are constant. Closedness is asserted for all triples of tangent vectors at all points.
• Non-triviality. The hypotheses are satisfiable: for $\lambda_a$ the standard real basis vectors of $\mathbb C^n$, the family $F(t)(x) = x + i t$ of flat real subtori of $\mathbb C^n/\Lambda$ meets every condition of the family structure, with $\theta^a_i = -\delta^a_i$ and $g_{ab} = \delta_{ab}$. The goal is therefore not vacuous, and it is also not trivially true: $\mathcal{J}$ is constant but $g_{ab}$ is not, so $d\omega_{\mathcal M}=0$ is a genuine condition on the family.

A complete development needs, beyond the definition item: the chain and product rules for fderiv on $\mathbb R^k$, symmetry of second derivatives, differentiation under the integral sign on a compact box, integration by parts for periodic functions on $[0,1]^n$, and the derivative of $\det$ and of matrix inversion. The last two, and the Hessian-implies-Kähler milestone, are reusable outside this mission. Contributions that replace the flat ambient by a general Kähler ambient chart, or that lift the model to Mathlib manifolds once differential forms exist there, are welcome and would supersede parts of this development.

Selected references

• A. Strominger, S.-T. Yau, E. Zaslow, Mirror symmetry is T-duality, Nuclear Physics B 479 (1996) 243–259. doi:10.1016/0550-3213(96)00434-8, arXiv:hep-th/9606040
• R. Harvey, H. B. Lawson, Calibrated geometries, Acta Mathematica 148 (1982) 47–157. doi:10.1007/BF02392726
• R. C. McLean, Deformations of calibrated submanifolds, Communications in Analysis and Geometry 6 (1998) 705–747. doi:10.4310/CAG.1998.v6.n4.a4
• N. J. Hitchin, The moduli space of special Lagrangian submanifolds, Annali della Scuola Normale Superiore di Pisa 25 (1997) 503–515. arXiv:dg-ga/9711002

Motivation

The local theory of curves describes what happens near one point; the global theory asks what a curve must satisfy because it closes up. Two classical statements make the difference visible. The isoperimetric inequality says that among all simple closed plane curves of a given length, the circle encloses the largest area — a question already settled in intent by the Greeks, but given a satisfactory proof only in the nineteenth century, and the short proof reproduced by do Carmo is E. Schmidt's from 1939. The four-vertex theorem says that the curvature of a simple closed convex curve has at least four critical points, so no convex oval has the curvature profile of a curve that just rises and falls once.

The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §1-7, "Global Properties of Plane Curves" (pp. 31–46): the area formula, equation (1) on p. 33; the isoperimetric inequality, Theorem 1 on p. 34; the theorem of turning tangents on p. 37; the lemma, equation (5) on p. 38; and the four-vertex theorem, Theorem 2 on p. 37.

This is the third mission of a series formalizing do Carmo's book, and shares the namespace DoCarmoDG with the earlier ones.

Setting

A closed plane curve of length $l$ is a regular map $\alpha : [0,l] \to \mathbb{R}^2$ whose derivatives of all orders agree at the two endpoints; equivalently, and as used here, a smooth $l$-periodic map $\alpha : \mathbb{R} \to \mathbb{R}^2$. It is parametrized by arc length when $|\alpha'(s)| = 1$ for all $s$, in which case $l$ is its length. It is simple when it has no self-intersection: $\alpha(t_1) \neq \alpha(t_2)$ for distinct $t_1, t_2 \in [0,l)$.

Write $J$ for rotation by $+\pi/2$, $J(a,b) = (-b,a)$. For a curve parametrized by arc length the signed curvature is

$$k(s) = \bigl\langle \alpha''(s),\, J\alpha'(s) \bigr\rangle,$$

which is do Carmo's convention of §1-5, Remark 1: the normal is chosen so that $\{\alpha', J\alpha'\}$ has the orientation of the natural basis, and then $\alpha'' = k\,J\alpha'$. A vertex is a parameter $t$ with $k'(t) = 0$. The curve is convex when, for every parameter $t$, the whole trace lies in one of the two closed half-planes bounded by the tangent line at $t$.

An angle function for $\alpha$ is a smooth $\theta$ with $\alpha'(s) = (\cos\theta(s), \sin\theta(s))$; the rotation index is $(\theta(l) - \theta(0))/2\pi$. The area bounded by a positively oriented simple closed curve is given by do Carmo's equation (1),

$$A = \frac{1}{2}\int_0^l \bigl(x\,y' - y\,x'\bigr)\,dt, \qquad \alpha = (x,y).$$

Formalization targets

Goal — Four-vertex theorem (do Carmo, Theorem 2, p. 37)

$$\alpha \ \text{simple closed convex} \quad \Longrightarrow \quad \#\{\,t \in [0,l) : k'(t) = 0\,\} \ge 4 .$$

Supporting statements

The three equivalent forms of the area formula (1); the existence of a smooth angle function; the identity $k = \theta'$; the theorem of turning tangents (the rotation index of a simple closed curve is $\pm 1$); the isoperimetric inequality $l^2 \ge 4\pi A$ with equality exactly for circles; and do Carmo's lemma (5), $\int_0^l (Ax + By + C)\,k'(s)\,ds = 0$, which drives the proof of the goal.

Significance

The isoperimetric inequality is the ancestor of a large family of geometric inequalities, and its sharp case characterizes the circle — the first instance of the pattern "extremal configuration is the round one" that recurs throughout geometry. The four-vertex theorem is a genuinely global statement with no local counterpart: locally, the curvature of a convex arc may be strictly monotone, and it is only the requirement that the curve close up convexly that forces four critical points. Its converse, for strictly positive curvature, was proved by H. Gluck in 1971; do Carmo notes that the theorem also holds for simple closed curves that are not convex, by a harder argument.

Mathlib contains integration, the winding number of a loop in the complex plane and the Jordan curve theorem, but it does not contain the signed curvature of a plane curve, the theorem of turning tangents in this form, the isoperimetric inequality for curves with its equality case, or the four-vertex theorem. What this mission adds is that vocabulary and machine-checked proofs of the four classical statements.

Difficulty

Each target fails for a different reason under the naive approach.

For the area formula, the identification of $\frac12\oint(x\,dy - y\,dx)$ with the area of the interior is exactly the Jordan-curve input that do Carmo declares he is assuming; the formalization avoids that dependency by defining the bounded area through the integral, so a solver has to prove only the integration-by-parts identities among the three forms of (1).

For the theorem of turning tangents, the difficulty is that a smooth lift $\theta$ of the tangent indicatrix must be produced and then shown to increase by exactly $\pm 2\pi$ over one period — a degree-theoretic statement about a loop in the circle, where simplicity of the curve is what excludes the values $0, \pm 2, \pm 3, \dots$.

For the isoperimetric inequality, Schmidt's proof compares the curve with a circle tangent to two parallel supporting lines and uses the arithmetic–geometric mean inequality; the equality discussion, which is where the characterization of the circle lives, is the delicate part.

For the four-vertex theorem, the obvious argument — "curvature on a compact interval attains a maximum and a minimum, so there are two vertices" — gives only two, and the whole content is the step from two to four. The lemma (5) supplies the contradiction: if $k'$ changed sign only at the maximum and the minimum, a suitable line $Ax + By + C = 0$ through those two points would make the integrand of (5) of one sign and not identically zero.

Formalization scope

Curves are smooth maps ℝ → EuclideanSpace ℝ (Fin 2), closedness being $l$-periodicity with $l > 0$, which is do Carmo's condition that the curve and all its derivatives agree at the endpoints. Unit speed is imposed globally, so the parameter is arc length and $l$ is the length. Simplicity is injectivity on the half-open period $[0,l)$. Convexity is stated per parameter: for each $t$ the trace lies in one closed half-plane of the tangent line at $t$, the choice of side being allowed to depend on $t$, as in the book's phrasing.

The area is defined by do Carmo's integral (1) rather than as the measure of the interior of the curve, so no Jordan curve theorem is presupposed; consequently the isoperimetric statement is formulated with the absolute value $|A|$, which makes it independent of the curve's orientation and equal to the enclosed area for a positively oriented simple curve. The equality case asserts that the trace lies on a circle of positive radius.

"At least four vertices" is formalized as the existence of four pairwise distinct parameters in $[0,l)$ at which $k'$ vanishes, which rules out the degenerate reading in which one vertex is counted several times.

Selected references

• Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition, Dover, 2016, §1-7 (area formula, eq. (1), p. 33; isoperimetric inequality, Theorem 1, p. 34; theorem of turning tangents, p. 37; lemma, eq. (5), p. 38; four-vertex theorem, Theorem 2, p. 37).
• E. Schmidt, Über das isoperimetrische Problem im Raum von n Dimensionen, Mathematische Zeitschrift 44 (1939), 689–788.
• H. Gluck, The converse to the four-vertex theorem, L'Enseignement Mathématique 17 (1971), 295–309.

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), 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.
• 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.