Number Theory

Why the two-item periodic JRP is hard

The joint replenishment problem (JRP) is the multi-item extension of the economic order quantity (EOQ) model. Each item is reordered periodically and pays its own ordering and holding costs, and a joint ordering cost is shared by items ordered at the same time. Before this work no hardness result was known for the periodic JRP (p. 10), even though no exact polynomial-time algorithm was known either (Schulz and Telha, arXiv:2007.09045; Operations Research, 2024, as Integer Factorization: Why Two-Item Joint Replenishment Is Hard).

The paper explains this through number theory. In the periodic JRP the joint cost is incurred every $\gcd(q_1, q_2)$ periods, so the objective contains a greatest common divisor of the decision variables. The paper's Theorem 2 states that, assuming the Riemann hypothesis, the two-item periodic JRP is NP-hard under randomized reductions. The proof composes two reductions:

• Shor's reduction from Partition to RangeDivisor ("does $M$ have a divisor in $[L, U]$?"), given in the paper's appendix and based on Shor (2011); this is where the Riemann hypothesis enters;
• a reduction from RangeDivisor to the two-item periodic JRP, whose correctness is Lemma 3 (pp. 13–14).

This mission formalizes Lemma 3. Mission 4 of this series formalizes the Partition half; missions 1 and 2 formalize the integer-factorization reductions behind Theorem 1.

Setting

A period is a positive integer $q$. An item with ordering cost $K$ and holding cost $H$ costs

$$\mathrm{EOQ}_{K,H}(q) = \frac{K}{q} + Hq$$

per unit time. The two-item periodic JRP (objective (3), p. 10) minimizes, over $q_1, q_2 \in \mathbb{Z}_+$,

$$\mathrm{JRP}(q_1, q_2) = \mathrm{EOQ}_{K_1,H_1}(q_1) + \mathrm{EOQ}_{K_2,H_2}(q_2) + \frac{K_0}{\gcd(q_1, q_2)}.$$

As a decision problem (p. 13), it asks whether some $(q_1, q_2)$ has cost at most a threshold $z$.

An instance of RangeDivisor (p. 12) is a triple of integers $M \ge U \ge L > 0$ satisfying

$$L + U < 2\sqrt{2LU};$$

it is a yes-instance when $M$ has a divisor $q$ with $L \le q \le U$.

Given such a triple, the instance $\mathrm{JRP}_{M,U,L}$ sets

$$K_0 = LU,\quad K_1 = 0,\quad H_1 = 1,\quad K_2 = M^3(M+1),\quad H_2 = M(M+1),$$

and the threshold is $z_{M,L,U} = L + U + 2M^2(M+1)$, where $2M^2(M+1) = \mathrm{EOQ}_{K_2,H_2}(M)$. Once item 2 is fixed at $q_2 = M$, item 1 solves problem (5):

$$\min_{q_1 \in \mathbb{Z}_+} \ \frac{LU}{\gcd(q_1, M)} + q_1 .$$

In Lean these objects are JRPHard.Aperiodic.eoq, JRPHard.Periodic.periodicCost, JRPHard.Periodic.coefK2, JRPHard.Periodic.coefH2 (shared with missions 1 and 2), and IsRangeDivisorInstance, HasDivisorIn, coefK0, rangeCost, threshold, obj5 and fConv in the namespace JRPHard.RangeDiv.

Formalization targets

Goal: Lemma 3

For every RangeDivisor instance $(M, L, U)$,

$$K_0,\ K_2,\ H_2 \le 2M^4 \quad\text{and}\quad \Big(\exists\, q \mid M,\ L \le q \le U\Big) \iff \Big(\exists\, q_1, q_2 \in \mathbb{Z}_+:\ \mathrm{JRP}_{M,U,L}(q_1, q_2) \le L + U + 2M^2(M+1)\Big).$$

Milestones (the steps of the proof, pp. 14–15)

1. Item 2 is pinned: every plan with $q_2 \ne M$ costs more than $z_{M,L,U}$.
2. $f(q) = LU/q + q$ is a lower bound on problem (5)'s objective, $f(L) = f(U) = L + U$, and $f$ is minimized at $\sqrt{LU}$.
3. $\gcd(q, M) \ne q \Rightarrow \gcd(q, M) \le q/2$.
4. If $\gcd(q, M) \ne q$, the objective of (5) at $q$ is at least $2\sqrt{2LU} > L + U$.
5. A divisor $q \in [L, U]$ of $M$ has objective at most $L + U$.
6. A period with objective at most $L + U$ divides $M$ and lies in $[L, U]$.

Significance

Lemma 3 is the step that carries hardness from number theory to inventory theory. With Shor's result it shows that, under the Riemann hypothesis, no polynomial-time exact algorithm for the two-item periodic JRP exists unless NP problems can be solved in randomized polynomial time. The paper concludes (p. 15) that no algorithm for the two-item problem may be simultaneously exact and polynomial on all inputs, so some concession, such as heuristics, must be made.

The result is proved in the paper; it has not been machine-checked. The mission produces a checked statement of the reduction's correctness with every coefficient explicit, and it corrects two imprecisions in the printed lemma (the threshold and the unspecified "sufficiently large" coefficients of item 2; see below). The objects (eoq, periodicCost) are the same ones used in mission 2 of this series.

Difficulty

Each step is elementary, but the statement mixes integer and real reasoning. The objective of (5) is not monotone or convex in $q$: its value jumps between $LU/q + q$ at divisors of $M$ and at least $2LU/q + q$ elsewhere. The argument must show that the gap between these two curves exceeds the window around $L + U$, and this is exactly what RangeDivisor's condition $L + U < 2\sqrt{2LU}$ provides. Without that condition a non-divisor can be cheaper than $L + U$ (for $L = 1$, $U = 100$, $M = 7$, the period $q = 14$ has objective $100/7 + 14 < 101$). The pinning of $q_2 = M$ also has to beat the slack $M + 2\sqrt{LU}$ against $L + U$, which is where $M \ge U$ is used.

Formalization scope

This mission formalizes the correctness of the reduction behind Theorem 2 (its JRP half, Lemma 3); polynomial running time is not formalized. Theorem 2 itself, Shor's NP-completeness of RangeDivisor under randomized reductions, and "one can construct in polynomial time" are not stated. What remains of the polynomial-time claim is the explicit coefficients and the bound $K_0, K_2, H_2 \le 2M^4$ (bit length at most $4\log_2 M + 2$).

Conventions:

• periods are natural numbers, and every quantified period is assumed positive (Lean's $K/0 = 0$ and $\gcd(0, M) = M$ would otherwise create spurious cheap plans);
• costs are real numbers; $L$, $U$, $M$ and the coefficients are natural numbers cast to $\mathbb{R}$;
• RangeDivisor's condition is stated with Real.sqrt exactly as printed;
• "the optimal value is at most $z$" is the decision form "some plan has cost at most $z$" (p. 13); the minimum is attained, so the two agree.

Two disclosed departures from the printed lemma:

• The threshold. The page writes "the optimal value of $\mathrm{JRP}_{M,U,L} \le L + U$". The two-item cost also contains item 2's term $2M^2(M+1)$, so the literal comparison never holds and would make the lemma false. The threshold is $z_{M,L,U} = L + U + 2M^2(M+1)$, the $z_{M,L,U}$ announced in §3.1.
• The item-2 coefficients. The page chooses "sufficiently large values of $K_2$ and $H_2$, as in … Lemma 2". The statement fixes Lemma 2's values $K_2 = M^3(M+1)$, $H_2 = M(M+1)$ rather than quantifying existentially, which would let any instance satisfy the lemma.

A formalization that drops the positivity of periods, states the threshold as $L + U$ on the full two-item cost, or leaves $K_2, H_2$ existential does not capture Lemma 3 and is ruled out.

No library beyond Mathlib (Nat.gcd, Real.sqrt) is needed. Proofs of the milestones, and alternative proofs of the goal, are welcome.

Selected references

• A. S. Schulz and C. Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, 2020; published as Integer Factorization: Why Two-Item Joint Replenishment Is Hard, Operations Research, 2024. https://arxiv.org/abs/2007.09045
• P. W. Shor, An NP-complete variant of factoring, Theoretical Computer Science Stack Exchange, 2011 (version 2011-03-01, as cited by the paper). https://cstheory.stackexchange.com/q/4785
• S. Arora and B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511804090

Background and motivation

Ring learning with errors (ring-LWE) is the algebraic variant of the learning-with-errors problem on which most practical lattice-based cryptography is built, including the key-encapsulation scheme ML-KEM standardized by NIST in 2024. Its hardness rests on the paper of Lyubashevsky, Peikert and Regev, On ideal lattices and learning with errors over rings (J. ACM 60(6), 2013, doi:10.1145/2535925; conference version at EUROCRYPT 2010). The paper's main theorem (Theorem 3.6, p. 19) is a polynomial-time quantum reduction from worst-case approximate shortest-vector problems on ideal lattices to the ring-LWE decision problem. Statements about reductions, running times and negligible probabilities are outside the scope of this mission.

What this mission formalizes is the algebraic tool both of the paper's reductions rest on, which the authors list among their main technical contributions (p. 7): a Chinese-remainder technique for clearing an ideal. An arbitrary ideal $\mathcal{I}$ of the ring of integers $R$ need not be principal, so a reduction that receives samples from a lattice $\mathcal{I}$ cannot simply divide by a generator. Lemmas 2.14 and 2.15 show that, modulo an ideal $\mathcal{J}$ such as $\langle q\rangle$, multiplication by a well-chosen $t\in\mathcal{I}$ identifies $R/qR$ with $\mathcal{I}/q\mathcal{I}$, and more generally $\mathcal{M}/\mathcal{J}\mathcal{M}$ with $\mathcal{I}\mathcal{M}/\mathcal{I}\mathcal{J}\mathcal{M}$ for every fractional ideal $\mathcal{M}$. Steps 1–3 of the BDD-to-LWE reduction of §4.2 consist of exactly these identifications. The authors note that the lemmas are "probably standard for experts in computational number theory" (p. 16); the formulation used in lattice cryptography is theirs, and it is reused throughout the later literature on algebraic lattices.

Setting

Let $K$ be a number field of degree $n$ and $R = \mathcal{O}_K$ its ring of integers. An integral ideal is a nonzero ideal $\mathcal{I}\subseteq R$ (the paper excludes $\{0\}$, footnote 2, p. 13). A fractional ideal is a set $\mathcal{I}\subset K$ such that $d\mathcal{I}$ is an integral ideal for some nonzero $d\in R$; the nonzero fractional ideals form a group under multiplication, and $\mathcal{I}^{-1}$ denotes the inverse. Two integral ideals are coprime when $\mathcal{I}+\mathcal{J} = R$.

For $t\in R$ the cleared ideal is $t\cdot\mathcal{I}^{-1} = \langle t\rangle\,\mathcal{I}^{-1}$. When $t\in\mathcal{I}$ it is an integral ideal, and "$t\cdot\mathcal{I}^{-1}$ is coprime to $\mathcal{J}$" means

$$t\cdot\mathcal{I}^{-1}\subseteq R \quad\text{and}\quad t\cdot\mathcal{I}^{-1}+\mathcal{J}=R .$$

For a fractional ideal $\mathcal{M}$ and $t\in\mathcal{I}$, the map $\theta_t(u) = t\cdot u$ sends $\mathcal{M}$ into $\mathcal{I}\mathcal{M}$, and therefore induces an $R$-linear map

$$\theta_t:\ \mathcal{M}\longrightarrow \mathcal{I}\mathcal{M}/\mathcal{I}\mathcal{J}\mathcal{M},\qquad u\mapsto t u \bmod \mathcal{I}\mathcal{J}\mathcal{M}.$$

The dual of a fractional ideal $\mathcal{L}$ is $\mathcal{L}^\vee = \{x\in K:\operatorname{Tr}(x\mathcal{L})\subseteq\mathbb{Z}\}$; $R^\vee$ is the codifferent, and $\mathcal{I}^\vee = \mathcal{I}^{-1}R^\vee$. For the cyclotomic field $K=\mathbb{Q}(\zeta)$, $\zeta$ a primitive $m$-th root of unity, $\tau_k$ ($k\in\mathbb{Z}_m^*$) is the automorphism with $\tau_k(\zeta)=\zeta^k$, and for a prime $q\equiv 1\pmod m$ with a primitive $m$-th root of unity $\omega\in\mathbb{Z}_q$ the primes above $q$ are $\mathfrak{q}_i = \langle q,\zeta-\omega^i\rangle$, $i\in\mathbb{Z}_m^*$. Calligraphic $\mathcal{I},\mathcal{J},\mathcal{M}$ of the paper are written I, J, M in the milestone texts.

Formalization targets

Goal: Lemma 2.15 (p. 17)

For nonzero ideals $\mathcal{I},\mathcal{J}\subseteq R$, $t\in\mathcal{I}$ with $t\cdot\mathcal{I}^{-1}$ coprime to $\mathcal{J}$, and a nonzero fractional ideal $\mathcal{M}$,

$$\theta_t:\ \mathcal{M}\to\mathcal{I}\mathcal{M}/\mathcal{I}\mathcal{J}\mathcal{M}\ \text{is surjective with kernel}\ \mathcal{J}\mathcal{M},\quad\text{so}\quad \mathcal{M}/\mathcal{J}\mathcal{M}\;\cong\;\mathcal{I}\mathcal{M}/\mathcal{I}\mathcal{J}\mathcal{M}$$

as $R$-modules, via $u\bmod\mathcal{J}\mathcal{M}\mapsto tu\bmod\mathcal{I}\mathcal{J}\mathcal{M}$.

Milestones

1. The existence content of Lemma 2.13 (a coprime pair has $c\in\mathcal{J}$ with $c\equiv 1\bmod\mathcal{I}$), already proved on the platform and entered as a reference. Lemma 2.12 (Chinese Remainder Theorem) is also included as a reference item, without being a milestone.
2. Lemma 2.14 (p. 16): for nonzero $\mathcal{I},\mathcal{J}$ there exists a nonzero $t\in\mathcal{I}$ with $t\cdot\mathcal{I}^{-1}$ coprime to $\mathcal{J}$.
3. The kernel claim of the proof of Lemma 2.15: $u\in\mathcal{M}$ and $tu\in\mathcal{I}\mathcal{J}\mathcal{M}$ imply $u\in\mathcal{J}\mathcal{M}$.
4. The surjectivity claim of the proof: if $c\in t\cdot\mathcal{I}^{-1}$ and $c\equiv1\bmod\mathcal{J}$, then for $v\in\mathcal{I}\mathcal{M}$, $cv\in t\mathcal{M}$ and $cv-v\in\mathcal{I}\mathcal{J}\mathcal{M}$.

Companion statements

• §4.2 step 2 (p. 23) and step 3 (p. 24): multiplication by $t$ is a bijection $R/qR\to\mathcal{I}/q\mathcal{I}$ and $\mathcal{I}^\vee/q\mathcal{I}^\vee\to R^\vee/qR^\vee$ for every integer $q\ge2$, the two instances of Lemma 2.15 the reduction uses.
• Lemma 2.16 (p. 17): $\tau_j(\mathfrak{q}_i)=\mathfrak{q}_{i/j}$ for all $i,j\in\mathbb{Z}_m^*$.
• Lemma 2.9 (p. 14): $n^{1/p}N(\mathcal{I})^{1/n}\le\lambda_1(\mathcal{I})\le n^{1/p}N(\mathcal{I})^{1/n}\sqrt{\Delta_K^{1/n}}$ in every $\ell_p$ norm, $p\in[1,\infty]$, stated as two items.

Significance

The isomorphism of Lemma 2.15 is what makes ideal lattices usable in worst-case to average-case reductions: it turns a discrete Gaussian sample from an arbitrary ideal $\mathcal{I}$ into a uniform element of the fixed ring $R_q$, and turns the ring-LWE secret in $R^\vee_q$ back into a coset of $q\mathcal{I}^\vee$. Lemma 2.16 is the corresponding tool for the search-to-decision reductions of §5, which move between the CRT components $R/\mathfrak{q}_i$ of a completely split $q$. Lemma 2.9 gives the scale of the lattices involved.

On the formal side, none of Lemmas 2.14–2.16 is stated on the platform or in Mathlib in this form. Mathlib has the Chinese remainder theorem for ideals, inverses of fractional ideals in Dedekind domains, trace duals with $\mathcal{I}^\vee=\mathcal{I}^{-1}R^\vee$, and the isomorphism $\mathrm{Gal}(\mathbb{Q}(\zeta_m)/\mathbb{Q})\cong(\mathbb{Z}/m\mathbb{Z})^*$; the mission connects these to the quotient modules and explicit primes that lattice cryptography works with. All statements are proved in the paper; what remains is the formal proof.

Difficulty

The obvious argument for Lemma 2.15 — both quotients have cardinality $N(\mathcal{J})$, so an injective map is bijective — needs the multiplicativity of the norm on fractional ideals and finiteness of the quotients, and still needs the kernel computation, which uses unique factorization: from $tu\in\mathcal{I}\mathcal{J}\mathcal{M}$ one has to cancel $\mathcal{I}$ and $\mathcal{M}$ inside the group of fractional ideals and then use coprimality of $t\mathcal{I}^{-1}$ and $\mathcal{J}$. Lemma 2.14 needs the factorization of $\mathcal{I}$ along the primes of $\mathcal{J}$ and a CRT choice of $t$; for $\mathcal{J}=0$ it would assert that $\mathcal{I}$ is principal, which is why the nonzero convention matters. In Lemma 2.16 the delicate point is the direction of the action: $\tau_j$ sends $\mathfrak{q}_i$ to $\mathfrak{q}_{i/j}$, not $\mathfrak{q}_{ij}$.

Formalization scope

• $K$ is a NumberField, $R$ is 𝓞 K, fractional ideals are FractionalIdeal (𝓞 K)⁰ K, and integral ideals are coerced into them. Ideals are nonzero, per footnote 2: every statement carries I ≠ ⊥ (and J ≠ ⊥, M ≠ 0 where the paper's convention applies); I ≠ ⊥ is essential because Lean defines $0^{-1}=0$. Two kernel/surjectivity milestones drop the nonzero hypotheses on $\mathcal{J}$ and $\mathcal{M}$, which only strengthens them.
• "$t\mathcal{I}^{-1}$ coprime to $\mathcal{J}$" is the predicate ClearedCoprime: $t\mathcal{I}^{-1}\le 1$ and $t\mathcal{I}^{-1}+\mathcal{J}=1$ in the semiring of fractional ideals.
• $\mathcal{M}/\mathcal{N}$ is the quotient of the $R$-module $\mathcal{M}$ by $\mathcal{N}\cap\mathcal{M}$; $\theta_t$ is the given $R$-linear map $\mathcal{M}\to\mathcal{I}\mathcal{M}/\mathcal{I}\mathcal{J}\mathcal{M}$. The goal states surjectivity and the kernel of this map. A bare statement that some isomorphism $\mathcal{M}/\mathcal{J}\mathcal{M}\cong\mathcal{I}\mathcal{M}/\mathcal{I}\mathcal{J}\mathcal{M}$ exists would be true for unrelated reasons and is not the lemma.
• Duals are Mathlib's FractionalIdeal.dual ℤ ℚ. $\tau_j$ is the inverse image of $j$ under IsCyclotomicExtension.Rat.galEquivZMod, acting on ideals by images; $\omega^i$ uses the representative of $i$ in $\{0,\dots,m-1\}$. $\ell_p$ norms sum over all $n$ complex embeddings; $\lambda_1$ bounds are phrased through nonzero elements of $\mathcal{I}$.
• Dropped algorithmic clauses: "such $t$ can be found efficiently" (Lemma 2.14), "this isomorphism may be efficiently inverted" (Lemma 2.15), the "deterministic polynomial-time algorithm" of Lemma 2.13 (only the existence of $c$ is referenced), and "which can be efficiently inverted" in §4.2. No complexity notion is encoded.
• Contributions welcome: proofs of the milestones, of the goal from them, and of the companion statements; general lemmas on quotients $\mathcal{M}/\mathcal{J}\mathcal{M}$ of fractional ideals are reusable beyond this mission.

Selected references

• V. Lyubashevsky, C. Peikert, O. Regev, On ideal lattices and learning with errors over rings, J. ACM 60(6), Article 43, 2013. https://doi.org/10.1145/2535925
• V. Lyubashevsky, C. Peikert, O. Regev, On ideal lattices and learning with errors over rings, EUROCRYPT 2010, LNCS 6110, pp. 1–23. https://doi.org/10.1007/978-3-642-13190-5_1
• O. Regev, On lattices, learning with errors, random linear codes, and cryptography, J. ACM 56(6), 2009. https://doi.org/10.1145/1568318.1568324
• NIST, FIPS 203: Module-Lattice-Based Key-Encapsulation Mechanism Standard, 2024. https://doi.org/10.6028/NIST.FIPS.203

Motivation

A basic question of additive combinatorics asks how a set grows under repeated addition. If a finite set $A$ in an abelian group satisfies $|A + B| \le \alpha |A|$ for some finite set $B$, how large can the iterated sumsets $hB = B + \cdots + B$ be? Plünnecke's inequality gives the answer used throughout the subject: some nonempty part of $A$ grows by at most a factor $\alpha$ per added copy of $B$. Combined with Ruzsa's triangle inequality it becomes the Plünnecke–Ruzsa inequality $|mB - nB| \le \alpha^{m+n}|A|$, which underlies Freĭman-type structure theorems, sum–product estimates and the polynomial Freĭman–Ruzsa programme.

Timeline.

• 1970: H. Plünnecke proves the inequality for iterated sumsets in abelian groups with a graph-theoretic method (commutative layered graphs and Menger's theorem).
• 1989: I. Z. Ruzsa simplifies Plünnecke's argument and combines it with the triangle inequality to bound $|mB - nB|$.
• 2011: G. Petridis gives a short elementary proof, without graphs (arXiv:1101.3507, Combinatorica 32, 2012). His argument also shows that one subset $X \subseteq A$ works for every number of summands $h$, and it extends to triple products $CXB$ in non-abelian groups.

Setting

Let $G$ be a group with finite subsets $A$, $B$, $C$. The product set is $AB = \{ab : a \in A,\ b \in B\}$, and $|\cdot|$ denotes cardinality. In an abelian group, written additively, the sumset is $A + B = \{a + b : a \in A,\ b \in B\}$, and for $h \ge 0$ the iterated sumset $hB$ is $B + \cdots + B$ with $h$ summands, $0B = \{0\}$. It is not the dilate $\{hb : b \in B\}$.

A nonempty subset $X \subseteq A$ has minimal growth under $B$ if

$$\frac{|XB|}{|X|} \le \frac{|ZB|}{|Z|} \quad\text{for every nonempty } Z \subseteq A.$$

Such an $X$ exists whenever $A$ is nonempty, since $A$ has finitely many subsets. In Lean, $G$ is a Group or AddCommGroup with decidable equality, the sets are Finset G with the pointwise operations of Mathlib (A * B, A + B, h • B), and cardinalities are #A cast to ℝ.

Formalization targets

Goal: Theorem 3.1

For finite $A$, $B$ in an abelian group with $A$ nonempty and $|A + B| \le \alpha|A|$, there is a nonempty $X \subseteq A$ with

$$|X + hB| \le \alpha^h |X| \qquad \text{for every } h \ge 0.$$

The point is the order of quantifiers: one $X$ serves all $h$.

Milestones

1. Proposition 2.1 (p. 5). If $|XB|/|X| \le |ZB|/|Z|$ for every $Z \subseteq X$, then $|CXB| \le \frac{|XB|}{|X|}\,|CX|$ for every finite $C$, in any group. This is already on the platform, proved, as FamousTheorems.pluennecke_petridis (additive notation, cross-multiplied), and enters the mission as a reference.
2. Theorem 1.5 (p. 3). In any group, $|AB| \le \alpha|A|$ with $A$ nonempty gives a nonempty $X \subseteq A$ with

$$|CXB| \le \alpha |CX| \quad\text{for every finite } C.$$

3. Inductive step of Theorem 3.1 (p. 7). For $X \subseteq A$ of minimal growth and $|A+B| \le \alpha|A|$:

$$|X + hB| \le \alpha\,|X + (h-1)B| \quad (h \ge 1).$$

Significance

Theorem 3.1 is the form of Plünnecke's inequality used in applications. Two consequences follow directly. Taking $A = B$ gives $|hB| \le \alpha^h|B|$ whenever $|2B| \le \alpha|B|$. Combining one $X$ for all $h$ with Ruzsa's triangle inequality gives $|mB - nB| \le \alpha^{m+n}|A|$ (Theorem 1.2 of the paper). With a separate $X$ for each $h$, the second step would need the same set for $m$ and $n$, and that is exactly what Theorem 3.1 provides. Theorem 1.5 is the non-abelian ingredient: missions 2 and 3 of this series apply it to obtain explicit Plünnecke-type bounds for $|B^h|$ and $|SB^h|$ in arbitrary groups.

Formalizing it. The results are proved and classical. Mathlib already contains Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul) and the Plünnecke–Ruzsa inequality Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add. Its proof runs through a private lemma that bounds $|X + hB|$ for one fixed minimiser, but no public statement in Mathlib or on the platform asserts Theorem 3.1 or Theorem 1.5 in the form "there exists a nonempty $X$ for all $h$" (respectively "for all $C$"). This mission adds those statements as reusable, citable nodes in the paper's numbering.

Difficulty

A first attempt iterates the hypothesis directly: $|A + 2B| \le \alpha|A + B|$ would follow if $A + B$ again grew by a factor $\alpha$ under $B$, but nothing controls the growth of $A + B$. The ratio $|ZB|/|Z|$ is not monotone in $Z$, and passing to subsets of $A$ can only help if the subset is chosen correctly. Choosing a different good subset for each $h$ gives Theorem 1.1 but loses the uniformity. The work is to show that one fixed subset controls all the products $CXB$ simultaneously, and in the non-abelian Theorem 1.5 to keep the order of the factors $C$, $X$, $B$ throughout.

Formalization scope

• Theorem 3.1 and the inductive step are stated in an AddCommGroup with DecidableEq. Theorem 1.5 is stated in a Group, with no commutativity, as on the page. The factor order $C \cdot X \cdot B$ is preserved.
• $hB$ is h • B (the $h$-fold sumset; 0 • B = {0}), and "for all $h$" ranges over all natural numbers, including the true case $h = 0$.
• $\alpha$ is an arbitrary real number; cardinalities are cast to ℝ. No hypothesis $\alpha \ge 1$ is added: it follows from the hypotheses once $A$ and $B$ are nonempty (with $B$ empty they force only $\alpha \ge 0$, and every conclusion is still true).
• Nonempty witness. The page says "there exists $X \subseteq A$". Since $\emptyset + hB = \emptyset$, the empty set would satisfy the printed statements trivially, and that formalization is ruled out: the goal and Theorem 1.5 assume $A$ nonempty and assert $X$ nonempty, matching the paper's choice of $X$ as a minimiser of a ratio defined on nonempty sets.
• Minimal growth in the step milestone is written cross-multiplied, $|X+B|\,|Z| \le |Z+B|\,|X|$, over nonempty $Z \subseteq A$; the step is stated for $h \ge 1$ with natural-number subtraction guarded by that hypothesis.
• Ruzsa's covering lemma and Ruzsa's triangle inequality, quoted in §4, are in Mathlib (Finset.ruzsa_covering_mul, Finset.ruzsa_triangle_inequality_mul_mulInv_mul) and are not items of this mission.
• No new definitions are needed. Welcome contributions: proofs of the three draft statements, and, separately, the deduction of Theorem 1.2 from Theorem 3.1.

Selected references

• G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups, arXiv:1101.3507v3, 2011; Combinatorica 32 (2012). https://arxiv.org/abs/1101.3507 , https://doi.org/10.1007/s00493-012-2818-5
• H. Plünnecke, Eine zahlentheoretische Anwendung der Graphentheorie, J. Reine Angew. Math. 243 (1970) 171–183. https://doi.org/10.1515/crll.1970.243.171
• I. Z. Ruzsa, An application of graph theory to additive number theory, Scientia, Ser. A 3 (1989) 97–109 (no online version).
• T. Tao, V. Vu, Additive Combinatorics, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511755149

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Rhin–Viola's bound.

Formalization target

The campaign template with the value $14.797074$ filled in: PiIrrationality.UpperBound (14.797074 : ℝ), i.e. $\mu(\pi) \le 14.797074$.

Value. The paper's Theorem states exactly that $7.398537$ is an effective irrationality measure of $\zeta(2)$, "whence $14.797074$ is an effective irrationality measure of $\pi$". The value is used as stated, with no rounding.

How the bound arises

Rhin and Viola prove that $7.398537$ is an effective irrationality measure of $\zeta(2) = \pi^2/6$, using a birational transformation acting on Beukers' double integrals and semi-infinite linear programming to optimise the arithmetic. A measure $\mu$ for $\pi^2$ gives $2\mu$ for $\pi$ (if $|\pi - p/q|$ is small then $|\pi^2 - p^2/q^2|$ is small with denominator $q^2$), hence their $2 \times 7.398537 = 14.797074$.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $14.797074$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• G. Rhin, C. Viola, On the irrationality measure of $\zeta(2)$, Ann. Inst. Fourier (Grenoble) 43 (1993), no. 1, 85–109. https://doi.org/10.5802/aif.1322
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

In 1985 R. S. Ward conjectured that "many (and perhaps all?) of the ordinary and partial differential equations that are regarded as being integrable or solvable may be obtained from the self-dual gauge field equations (or its generalizations) by reduction". The self-dual Yang–Mills (SDYM) equations are therefore often called the master integrable system: choosing a gauge algebra and a symmetry group to reduce by produces, on the one hand, the classical soliton equations and the Painlevé transcendents, and on the other — once infinite-dimensional gauge algebras are allowed — a family of third-order equations whose solutions have movable natural barriers and are therefore not of Painlevé type.

This mission formalizes the endpoint of one such reduction chain, as surveyed by Ablowitz, Chakravarty and Halburd, Integrable systems and reductions of the self-dual Yang–Mills equations, J. Math. Phys. 44 (2003) 3147–3173, Section V. Reducing SDYM to functions of a single variable gives the Nahm equations; taking the gauge algebra to be the divergence-free vector fields on $S^3$ turns them into a matrix flow which, after diagonalizing the symmetric part, becomes the generalized Darboux–Halphen system. Its trace is governed by the Chazy equation, written down by Chazy in 1909, and — this is the paper's historical observation — the Chazy equation is equivalent to the differential system Ramanujan derived in 1916 for the Eisenstein series $P = E_2$, $Q = E_4$, $R = E_6$. Chazy and Ramanujan worked on the same equation at nearly the same time and apparently did not know it.

Setting

Throughout, $t$ and $q$ are complex variables and all functions are complex-valued; a "solution on $s$" means the stated derivative identities hold at every point of a set $s \subseteq \mathbb{C}$.

The classical Chazy equation is the third-order equation

$$\frac{d^3y}{dt^3} = 2y\,\frac{d^2y}{dt^2} - 3\left(\frac{dy}{dt}\right)^2 .$$

The classical Darboux–Halphen system is the first-order system for $\omega_1,\omega_2,\omega_3$

$$\dot\omega_1 = \omega_2\omega_3 - \omega_1(\omega_2+\omega_3),$$

together with its two cyclic images. It arose in Darboux's study of triply orthogonal surfaces and was solved by Halphen. Its generalized form adds a term $\tau^2 = \tau_1^2+\tau_2^2+\tau_3^2$ to each right-hand side, where $\dot\tau_1 = -\tau_1(\omega_2+\omega_3)$ and cyclically.

Ramanujan's system is

$$q\frac{dP}{dq} = \frac{P^2-Q}{12},\qquad q\frac{dQ}{dq} = \frac{PQ-R}{3},\qquad q\frac{dR}{dq} = \frac{PR-Q^2}{2},$$

satisfied by $P(q) = 1-24\sum_{n\ge1}\sigma_1(n)q^n$, $Q(q) = 1+240\sum_{n\ge1}\sigma_3(n)q^n$, $R(q) = 1-504\sum_{n\ge1}\sigma_5(n)q^n$, where $\sigma_k(n)=\sum_{d\mid n}d^k$.

Finally, the $3\times3$ matrix flow obtained from the Nahm equations with the $\mathrm{diff}(S^3)$ gauge algebra is

$$\dot M = (\operatorname{Adj} M)^{T} + M^{T}M - (\operatorname{Tr} M)M,\qquad \operatorname{Adj}M = (\det M)M^{-1},$$

and the generalized Chazy equation with parameter $n$ is

$$\frac{d^3y}{dt^3} - 2y\frac{d^2y}{dt^2} + 3\left(\frac{dy}{dt}\right)^2 = \frac{4}{36-n^2}\left(6\frac{dy}{dt}-y^2\right)^2 .$$

Formalization targets

Goal — the Chazy–Ramanujan correspondence (eqs. (78) and (71))

If $P,Q,R$ satisfy Ramanujan's system on a region of the punctured $q$-plane, then

$$y(t) := i\pi P\!\left(e^{2\pi i t}\right)$$

satisfies the classical Chazy equation on the preimage region. In particular $y(t)=i\pi E_2(t)$ is a solution of the Chazy equation, and knowing the general solution of Chazy gives the general solution of Ramanujan's system.

Supporting targets

The milestone list covers the reduction chain in both directions: the matrix flow $\dot M = (\operatorname{Adj}M)^T + M^TM-(\operatorname{Tr}M)M$ and its reduction to the Darboux–Halphen system (eqs. (51)–(54)), the first integrals (55), the passage $y = -2(\omega_1+\omega_2+\omega_3)$ from Darboux–Halphen to Chazy and back through the roots of a cubic, the $\mathrm{SL}(2)$ symmetry (73) of the Chazy equation, Rankin's fourth-order equation for the discriminant cusp form, the change of variable $q=e^{2i\tau}$ between the two forms of Ramanujan's system, and the generalized Chazy equation (81).

Significance

The Chazy equation is the bridge between integrable systems and the theory of modular forms. Its particular solution $y = i\pi E_2$ makes the quasi-modularity of the second Eisenstein series an ODE statement; via $y = \tfrac12 (\log\Delta)'$ it turns into Rankin's homogeneous fourth-order equation for the discriminant cusp form $\Delta$, whose Fourier coefficients are the Ramanujan $\tau$-function. The $\mathrm{SL}(2,\mathbb{Z})$ action on solutions is exactly the weight-2 quasi-modular transformation law. In the other direction, the general solution of Chazy is a ratio of hypergeometric functions with a movable natural barrier, which is why these reductions are used as the standard counterexample to the identification of integrability with the Painlevé property.

None of this material is currently in Mathlib: there is no Chazy equation, no Darboux–Halphen system, no Ramanujan differential system, and no Eisenstein-series ODE. The mission builds that layer from scratch. Each statement is a closed-form differential identity, so the development is self-contained: it needs no analytic continuation theory, no modular-forms library, and no existence theory for ODEs. What a solver must supply is careful derivative bookkeeping and polynomial algebra.

Status honesty: every statement in this mission is a classical, published result — Darboux, Halphen, Chazy (1909–1911), Ramanujan (1916), Rankin (1956), and Ablowitz–Chakravarty–Halburd (1990s–2003). Nothing here is open mathematics. What is open is the machine-checked proof; to the captain's knowledge no formalization of these identities exists.

Difficulty

The obvious approach — "differentiate three times and call ring" — fails for two reasons. First, the statements are about functions, not about polynomials: each differentiation step requires producing the derivative of a product, a quotient, or a composition from the hypotheses, and only then is the resulting algebraic identity a ring problem. Second, two of the targets go against the flow of the hypotheses. Recovering the Darboux–Halphen system from a Chazy solution means recovering $\dot\omega_i$ from the derivatives of the three elementary symmetric functions of the $\omega_i$: this is a linear system whose matrix is a Vandermonde matrix in $\omega_1,\omega_2,\omega_3$, invertible precisely because the roots are assumed distinct — which is why the distinctness hypothesis is not decoration. Similarly, the matrix milestone needs the conjugation-equivariance of $M \mapsto (\operatorname{Adj}M)^T + M^TM - (\operatorname{Tr}M)M$, which holds for the transpose only because the conjugating matrix is complex orthogonal.

Formalization scope

Everything is over $\mathbb{C}$, matching the paper. Solutions are represented pointwise on an arbitrary set $s \subseteq \mathbb{C}$ rather than on all of $\mathbb{C}$, because the solutions of interest have movable singularities and natural barriers; no openness, holomorphy or connectivity is assumed unless a statement needs it.

Higher derivatives are carried as explicit extra function arguments joined by HasDerivAt hypotheses rather than through iterated deriv. This avoids junk values entirely: a statement never asserts anything about the value of a derivative that does not exist. The same convention is used for the matrix flow, where the derivative is imposed entrywise, so that no norm or normed-space structure on the space of matrices needs to be chosen.

Divisions are arranged so that no denominator can vanish under the stated hypotheses: Ramanujan's system is written in the form $q\,dP/dq = (P^2-Q)/12$, with no division by $q$; the generalized Chazy equation carries the hypothesis $n^2 \ne 36$; and the first-integral and discriminant statements carry explicit nonvanishing hypotheses.

There is no trivializing formalization available here. Every statement is an implication between two systems of differential equations whose hypotheses are satisfied by the classical explicit solutions ($P=E_2$, $Q=E_4$, $R=E_6$ for the Ramanujan system; Halphen's solutions for Darboux–Halphen), so none of them is vacuous, and none is an identity that holds for arbitrary functions.

A complete development needs only Mathlib's derivative calculus (HasDerivAt and its product, quotient and composition rules), Complex.exp, and Matrix.adjugate with the basic adjugate identities. Contributions of reusable pieces are welcome: in particular a clean statement of the derivative of the elementary symmetric functions of a triple of functions, and the Vandermonde inversion step, would both be of use beyond this mission.

Selected references

• M. J. Ablowitz, S. Chakravarty, R. G. Halburd, Integrable systems and reductions of the self-dual Yang–Mills equations, J. Math. Phys. 44 (2003) 3147–3173. doi:10.1063/1.1586967
• J. Chazy, Sur les équations différentielles du troisième ordre et d'ordre supérieur dont l'intégrale générale a ses points critiques fixes, Acta Math. 34 (1911) 317–385. doi:10.1007/BF02393131
• S. Ramanujan, On certain arithmetical functions, Trans. Cambridge Philos. Soc. 22 (1916) 159–184.
• G. Halphen, Sur un système d'équations différentielles, C. R. Acad. Sci. Paris 92 (1881) 1101–1103.
• R. A. Rankin, The construction of automorphic forms from the derivatives of a given form, J. Indian Math. Soc. 20 (1956) 103–116.
• M. J. Ablowitz, S. Chakravarty, R. G. Halburd, The generalized Chazy equation and Schwarzian triangle functions, Asian J. Math. 2 (1998) 619–624. doi:10.4310/AJM.1998.v2.n4.a1
• R. S. Ward, Integrable and solvable systems, and relations among them, Philos. Trans. R. Soc. London A 315 (1985) 451–457. doi:10.1098/rsta.1985.0051

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

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.