Motivation

Many questions about polynomial equations — which equations can be solved by radicals, which geometric constructions are possible with ruler and compass, how the roots of a polynomial are related — become questions about the symmetries of a field extension. The fundamental theorem of Galois theory, going back to Évariste Galois, is the dictionary that makes this possible: for a finite Galois extension it matches intermediate fields with subgroups of a finite group, so that questions about fields become questions in finite group theory. The same dictionary underlies Kummer theory and class field theory, and it is the step that turns the unsolvability of the general quintic (Abel–Ruffini) into a statement about solvable groups.

This mission follows the Wikipedia article Fundamental theorem of Galois theory (revision 1345286594): its main statement, its list of properties of the correspondence, three of its worked examples, and its section on the infinite case.

Setting

A field extension $E/F$ is a field $E$ with a field $F$ inside it; it is finite when $E$ is finite-dimensional as an $F$-vector space, of dimension $[E:F]$. An intermediate field is a field $K$ with $F \subseteq K \subseteq E$. The automorphism group $G = \operatorname{Aut}(E/F)$ is the group of field automorphisms $\sigma$ of $E$ with $\sigma(a) = a$ for every $a \in F$.

The two maps of the correspondence are:

• for a subgroup $H \le G$, the fixed field $E^H = \{x \in E : \sigma(x) = x \text{ for all } \sigma \in H\}$;
• for an intermediate field $K$, the fixing subgroup $\operatorname{Aut}(E/K) = \{\sigma \in G : \sigma(x) = x \text{ for all } x \in K\}$.

The extension is Galois when it is normal and separable; for a finite extension this is equivalent to $|G| = [E:F]$. When $E/F$ is Galois, $G$ is written $\operatorname{Gal}(E/F)$.

For an infinite algebraic Galois extension, $G$ carries the Krull topology: the coarsest topology for which each restriction map $G \to \operatorname{Gal}(L/F)$, with $L/F$ a finite Galois subextension and $\operatorname{Gal}(L/F)$ discrete, is continuous.

Formalization targets

Goal: Galois if and only if the correspondence is one-to-one

For a finite extension $E/F$,

$$E/F \text{ is Galois} \iff \Big(\forall K,\ E^{\operatorname{Aut}(E/K)} = K\Big) \text{ and } \Big(\forall H \le G,\ \operatorname{Aut}(E/E^H) = H\Big).$$

Milestones

1. Basic form (forward direction of the goal, already on the platform): for finite Galois $E/F$ the two maps are mutually inverse.
2. Non-Galois case: for finite non-Galois $E/F$, $H \mapsto E^H$ is injective but not surjective, $K \mapsto \operatorname{Aut}(E/K)$ is surjective but not injective, and $F$ is not the fixed field of any subgroup.
3. Inclusion reversing: $H_1 \le H_2 \iff E^{H_2} \subseteq E^{H_1}$.
4. Degrees: $[E : E^H] = |H|$ and $[E^H : F] = [G : H]$.
5. Normality: $E^H/F$ is normal $\iff$ $H$ is a normal subgroup.
6. Quotient: if $H$ is normal, restriction to $E^H$ induces an isomorphism $G/H \cong \operatorname{Gal}(E^H/F)$.
7. Example 1: $K = \mathbb{Q}(\sqrt2, \sqrt3)$ has degree $4$, is Galois, its Galois group is a Klein four-group, and it has five subgroups and five intermediate fields.
8. Example 2: the splitting field of $x^3 - 2$ over $\mathbb{Q}$ has degree $6$, Galois group $\cong S_3$, six subgroups and six intermediate fields.
9. Example 4: $\mathbb{Q}(\sqrt[3]{2})$ has degree $3$, trivial automorphism group, and is not Galois.
10. Infinite case, well-definedness: for any Galois extension, $\operatorname{Aut}(E/K)$ is closed in the Krull topology.
11. Infinite case (already on the platform): intermediate fields correspond bijectively to closed subgroups.

Significance

The result. The correspondence turns the lattice of intermediate fields of a finite Galois extension into the (reversed) lattice of subgroups of a finite group, with degrees matching indices and normal subextensions matching normal subgroups. This is the tool used to classify subfields, to compute Galois groups of explicit polynomials, and to prove that solvability by radicals corresponds to solvability of the Galois group.

Formalizing it. The theorems are classical, and Mathlib contains formal proofs of the general finite and infinite correspondences (for example IsGalois.intermediateFieldEquivSubgroup and the InfiniteGalois namespace). This mission's contribution is a statement set indexed by the source: the converse direction ("only if Galois") as the goal, the non-Galois behaviour, each listed property, and the concrete examples of the article. The explicit examples require genuine computation: degrees of towers, minimal polynomials, and counting subgroups and subfields.

Difficulty

The general statements reduce to Artin's theorem and a degree count, but the non-Galois milestone asks for four separate claims about injectivity and surjectivity, each needing the correct direction of Artin's theorem. The examples cannot be settled by a general principle: showing that $\mathbb{Q}(\sqrt2,\sqrt3)$ has exactly five intermediate fields, or that the splitting field of $x^3-2$ has degree $6$, requires irreducibility arguments and an explicit transfer through the correspondence. Showing that $\mathbb{Q}(\sqrt[3]2)$ has no non-trivial automorphism requires knowing that the other two roots of $x^3-2$ are not real.

Formalization scope

All statements use Mathlib's IntermediateField F E, IntermediateField.fixedField, IntermediateField.fixingSubgroup, the automorphism group E ≃ₐ[F] E, and IsGalois (normal and separable). Finite means FiniteDimensional F E. Subgroups in the finite statements range over all subgroups; in the infinite case the Krull topology is Mathlib's standard topology on E ≃ₐ[F] E. Degrees are Module.finrank, orders are Nat.card, and the index is Subgroup.index. The concrete fields of the examples are taken inside $\mathbb{R}$ (for $\mathbb{Q}(\sqrt2,\sqrt3)$ and $\mathbb{Q}(\sqrt[3]2)$, with $\sqrt[3]2 = 2^{1/3}$ the real cube root) or as the abstract splitting field (for $x^3-2$). The quotient milestone takes the normality of $H$ and of $E^H/F$ as instance hypotheses; they are equivalent by milestone 5, so neither is vacuous.

The article's Example 3 (the anharmonic group acting on $\mathbb{C}(\lambda)$) and the "Applications" section are out of scope for this first mission. No new definitions are needed; contributions of proofs for any milestone are welcome.

Selected references

• Wikipedia, Fundamental theorem of Galois theory, revision 1345286594. https://en.wikipedia.org/w/index.php?title=Fundamental_theorem_of_Galois_theory&oldid=1345286594
• J. S. Milne, Fields and Galois Theory, Kea Books, 2022. https://www.jmilne.org/math/CourseNotes/ft.html
• The Stacks Project, Theorem 9.21.7 (Fundamental theorem of Galois theory). https://stacks.math.columbia.edu/tag/09DW
• The Stacks Project, Theorem 9.22.4 (Fundamental theorem of infinite Galois theory). https://stacks.math.columbia.edu/tag/0BML
• L. Ribes, P. Zalesskii, Profinite Groups, Springer, 2010. ISBN 978-3-642-01641-7.

Motivation

Polynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$ that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of Chen--Tan.

The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family $\tau(C,\Phi)$ carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.

Setting

Fix $\ell\ge2$ and the complex symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$. The relevant maximal parabolic subalgebra has an abelian nilradical $\mathfrak n$. Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free $U(\mathfrak n)$-module can consequently be modeled on that polynomial ring.

The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar $C\in\mathbb C$ and a polynomial parameter $\Phi$. Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family $\tau(C,\Phi)$ realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.

Formalization targets

Common polynomial-module family

Prove that for every $\ell\ge2$ there is one generator presentation and one family

$$(C,\Phi)\longmapsto \tau(C,\Phi)$$

of $\mathfrak{sp}_{2\ell}(\mathbb C)$-representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that $\tau(C,\Phi)$ is a weight module exactly when $\Phi$ is constant, and the stated simplicity criterion outside the exceptional arithmetic set

$$\left\{\frac{\ell+1}{2}-\frac{n}{2}:n\in\mathbb Z_{>0}\right\}.$$

For exceptional $C$, prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family $\tau$.

Significance

The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.

Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.

Difficulty

The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.

The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.

Formalization scope

The mission works over $\mathbb C$ with natural rank $\ell\ge2$. The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.

The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family $\tau$. Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's sorry. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.

Selected references

• Yang Chen and Haijun Tan, Simple $\mathfrak{sp}_{2\ell}(\mathbb C)$-modules which are free over an abelian nilradical, Journal of Algebra 697 (2026), 341--372, Theorems 1.1--1.3 (formal Theorems 3.7, 3.8, 4.7, 4.9, and 5.2). DOI
• G. Shen, foundational work on mixed-product constructions for modules over Lie algebras of Cartan type, cited in the source paper for the Shen--Larsson functor.

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

Hilbert's Nullstellensatz ("theorem of zeros") is the basic link between algebra and geometry. It was proved by David Hilbert in his second major paper on invariant theory in 1893, after his 1890 paper that proved the basis theorem, and it is a foundational result of algebraic geometry. It gives an algebraic criterion for when a system of polynomial equations over an algebraically closed field has a solution, and an algebraic criterion for when one polynomial vanishes wherever a given family does. Every dictionary between affine varieties and ideals — points and maximal ideals, algebraic sets and radical ideals, irreducible sets and prime ideals — is a consequence.

This mission follows the Wikipedia article Hilbert's Nullstellensatz (snapshot of 27 September 2026): its introduction, its section Formulations, the statement of Zariski's lemma from Proofs, and the first theorem of Generalizations (finitely generated algebras over Jacobson rings).

Setting

Let $k$ be a field and $K$ an algebraically closed field extension of $k$ (every non-constant polynomial over $K$ has a root in $K$). Write $k[X_1,\dots,X_n]$ for the polynomial ring in $n$ variables. A point is an $n$-tuple $a = (a_1,\dots,a_n) \in K^n$, and $f(a)$ is the value of a polynomial $f$ at $a$.

• For an ideal $J$, the algebraic set (zero locus) is $\mathrm V(J) = \{a \in K^n : f(a) = 0 \text{ for all } f \in J\}$.
• For $U \subseteq K^n$, the vanishing ideal is $\mathrm I(U) = \{p : p(a) = 0 \text{ for all } a \in U\}$.
• The radical of $J$ is $\sqrt J = \{p : p^r \in J \text{ for some } r \in \mathbb N\}$.
• For $a \in K^n$, $\mathfrak m_a = (X_1 - a_1, \dots, X_n - a_n)$ is the ideal of the point.
• A subset $W \subseteq K^n$ is irreducible (Zariski topology) if it is nonempty and is not covered by two algebraic sets without lying in one of them.
• A commutative ring is Jacobson if every radical ideal is an intersection of maximal ideals.

Formalization targets

Goal: the Nullstellensatz

If $p \in k[X_1,\dots,X_n]$ vanishes on $\mathrm V(J) \subseteq K^n$, then

$$\exists\, r \in \mathbb N,\qquad p^r \in J.$$

This is the statement of the article's section Formulations, with the coefficient field $k$ and the algebraically closed field $K$ allowed to differ.

Milestones

1. Systems of equations. Over algebraically closed $K$: a system $f_1 = \dots = f_m = 0$ has no solution in $K^n$ iff $g_1 f_1 + \dots + g_m f_m = 1$ for some $g_i$; and $f$ vanishes on all solutions iff $f^r = g_1 f_1 + \dots + g_m f_m$ for some $r$ and $g_i$.
2. Geometric form. $\mathrm I(\mathrm V(J)) = \sqrt J$.
3. Weak Nullstellensatz. A proper ideal of $k[X_1,\dots,X_n]$ has a common zero in $K^n$; algebraic closedness is needed, as $(X^2+1) \subseteq \mathbb R[X]$ shows; for $K = \mathbb C$, $n = 1$ this is the fundamental theorem of algebra: $P$ has a complex root iff $\deg P \ne 0$.
4. Correspondences. $\mathrm V$ is an order-reversing bijection from radical ideals onto algebraic sets, with inverse $\mathrm I$; $\mathrm I(\{a\}) = \mathfrak m_a$ is maximal; every maximal ideal of $K[X_1,\dots,X_n]$ is some $\mathfrak m_a$; an algebraic set $W$ is irreducible iff $\mathrm I(W)$ is prime.
5. Intersections. $\sqrt J = \bigcap_{\mathfrak m \supseteq J} \mathfrak m = \bigcap_{a \in \mathrm V(J)} \mathfrak m_a$.
6. Zariski's lemma. A field finitely generated as an algebra over a field $K$ is a finite extension of $K$.
7. Jacobson rings. A finitely generated algebra $S$ over a Jacobson ring $R$ is Jacobson, and for a maximal ideal $\mathfrak n \subseteq S$, $\mathfrak n \cap R$ is maximal and $S/\mathfrak n$ is finite over $R/(\mathfrak n \cap R)$.

Significance

The Nullstellensatz makes the zero sets of polynomial systems accessible through ideals: solvability of a system becomes the ideal-membership question $1 \in J$, and the geometry of algebraic sets becomes the algebra of radical ideals. Consequences include the identification of the points of $K^n$ with the maximal ideals of $K[X_1,\dots,X_n]$, the description of irreducible algebraic sets by prime ideals, and the reduction of the fundamental theorem of algebra to the case $n=1$. The Jacobson-ring version extends the first equality of the intersection formula to every finitely generated algebra over a field.

All statements here are classical and proved. Mathlib already contains versions of several of them in its own vocabulary (Jacobson rings, Zariski's lemma, and a Nullstellensatz over an algebraically closed coefficient field). What this mission adds is a single set of statements matching the article's formulations: the version with separate fields $k \subseteq K$, the explicit systems-of-equations form, the point-ideal and irreducibility correspondences over $K^n$, and the intersection formula — and, for solvers, the bridges from these concrete statements to Mathlib's abstract ones.

Difficulty

The inclusion $\sqrt J \subseteq \mathrm I(\mathrm V(J))$ is immediate; the content is the reverse inclusion, which requires producing a point of $K^n$ from purely algebraic data. When $k \ne K$ the ideal $J$ lives over $k$ while the points live over $K$, so a result stated only for $K[X_1,\dots,X_n]$ does not apply directly: an ideal of $k[X]$ must be related to the ideal it generates in $K[X]$ without losing membership information. For the correspondences, the explicit ideals $\mathfrak m_a$ and the closed-set definition of irreducibility must be matched with the abstract notions (maximal spectrum, irreducible closed subsets) used in the library.

Formalization scope

• Points of $K^n$ are functions $\mathrm{Fin}\,n \to K$; polynomials are MvPolynomial (Fin n) k. When $k \ne K$, $K$ is a $k$-algebra and evaluation of a polynomial over $k$ at a point of $K^n$ goes through $k \to K$.
• $n = 0$ is allowed throughout; so is the unit ideal $J = k[X]$, where $\mathrm V(J) = \emptyset$ and empty intersections of ideals are the whole ring.
• Irreducibility is stated through closed sets (algebraic sets) without putting a topology on $K^n$. The degree in the $n=1$ statement is Mathlib's Polynomial.degree, with $\deg 0 = -\infty$.
• In the goal, the exponent $r$ may be $0$; that witness only works when $J$ is the unit ideal, so it does not trivialize the statement.
• Out of scope: the proofs via resultants and Gröbner bases, the effective Nullstellensatz, Lang's infinite-variable version, the scheme-theoretic generalizations, and the projective and analytic Nullstellensätze.
• Reusable output: the definitions $\mathrm V$, $\mathrm I$, algebraic set, irreducible set and $\mathfrak m_a$, and bridges to Mathlib's MvPolynomial.zeroLocus, MvPolynomial.vanishingIdeal, and IsJacobsonRing.

Selected references

• D. Hilbert, Ueber die vollen Invariantensysteme, Mathematische Annalen 42 (1893).
• Wikipedia contributors, Hilbert's Nullstellensatz. https://en.wikipedia.org/wiki/Hilbert%27s_Nullstellensatz
• M. F. Atiyah, I. G. Macdonald, Introduction to Commutative Algebra, Addison-Wesley, 1969, Chapters 5 and 7.
• D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Springer GTM 150, 1995, Chapter 4.

Motivation

The real Clifford algebra $\mathrm{Cl}(6,0)$ is the smallest Euclidean Clifford algebra whose full structure carries a nontrivial multiplicity-eight representation-theoretic decomposition, and it has become a recurring object in programs that build internal gauge and family structure from Clifford generators rather than imposing it by hand. Within such programs, the single most basic representation-theoretic question one can ask about the algebra is: how does a distinguished $\mathfrak{su}(2)$ subalgebra, acting by the adjoint action, decompose the odd part of the algebra as a representation?

This mission answers that question exactly, for the specific triple of bivectors built on the index set $\{0,2,5\}$. The computation was carried out structurally (by splitting active indices from spectator indices) in the LeanProofs research program in 2026 and recorded with exact multiplicities; no machine-checked proof exists yet. The purpose here is to close that gap: the result is finite-dimensional linear algebra, completely within reach of a Lean 4 + Mathlib development, and every constant in it is explicit.

Setting

Fix $\mathbb{R}^6$ with its standard inner product and the associated quadratic form $Q_{60} = \mathrm{diag}(1,1,1,1,1,1)$, and let $\mathrm{Cl}(6,0) = \mathrm{CliffordAlgebra}(Q_{60})$ be the real Clifford algebra generated by symbols $e_0,\dots,e_5$ with

$$e_i^2 = 1, \qquad e_i e_j = -e_j e_i \ \ (i \neq j).$$

The algebra is $\mathbb{Z}$-graded in the usual sense: it is the direct sum of its grade-$k$ subspaces, spanned by products of $k$ distinct generators, of dimension $\binom{6}{k}$. The odd sector is the linear span of the odd grades,

$$\mathrm{Cl}^-(6,0) \;=\; \mathrm{grade}_1 \oplus \mathrm{grade}_3 \oplus \mathrm{grade}_5, \qquad \dim_{\mathbb{R}} \mathrm{Cl}^-(6,0) = 6 + 20 + 6 = 32.$$

On it, register three bivectors and their halved adjoint actions:

$$E_1 = e_0 e_2, \quad E_2 = e_2 e_5, \quad E_3 = e_0 e_5, \qquad T_i = \tfrac{1}{2}\,\mathrm{ad}_{E_i},$$

where $\mathrm{ad}_{X}(Y) = XY - YX$. The triple satisfies the $\mathfrak{su}(2)$ relations $[E_1,E_2]=2E_3$ and cyclic permutations, so the $T_i$ generate a copy of $\mathfrak{su}(2)$ with $[T_1,T_2]=T_3$ cyclically. The associated quadratic Casimir is the endomorphism

$$C \;=\; -(T_1^2 + T_2^2 + T_3^2).$$

Because each $E_i$ is even, every $T_i$ preserves the odd sector, and so does $C$.

Formalization targets

Goal — the Casimir spectrum with exact multiplicities

$$C\big|_{\mathrm{Cl}^-(6,0)} \ \text{has eigenvalue } 2 \text{ with multiplicity } 24 \ \text{and eigenvalue } 0 \text{ with multiplicity } 8,$$

the two eigenspaces spanning the whole odd sector. Equivalently, as a representation of the generated $\mathrm{Spin}(3) \cong \mathrm{SU}(2)$,

$$\mathrm{Cl}^-(6,0) \;\cong\; 8\,V_{j=1} \;\oplus\; 8\,V_{j=0},$$

eight copies of the spin-1 module and eight copies of the trivial module. The goal deliberately asserts only the eigenspace dimensions and their spanning property — the decomposition shape — not any particular basis or pairing.

Stronger — the Cartan weight decomposition

$$T_3\text{-weights on } \mathrm{Cl}^-(6,0): \quad 0 \ \text{(multiplicity } 16\text{)}, \qquad +1 \ \text{and} \ -1 \ \text{(multiplicity } 8 \text{ each)},$$

the three weight spaces spanning the sector. This refines the goal: each $j=1$ copy contributes weights $-1,0,+1$ and each $j=0$ copy contributes weight $0$.

Significance

The result itself. The spectrum pins down exactly how an $\mathfrak{su}(2)$ acting from inside the algebra sees the odd sector: not irreducibly, but as a clean $8 \oplus 8$ multiplicity split between spin-1 and spin-0. In the LeanProofs program this decomposition is load-bearing for everything downstream that distinguishes "active" indices from "spectator" indices — the multiplicity $8$ is the number of spectator degrees of freedom, and its appearance in the spectrum is what makes the split structural rather than coincidental. The weight decomposition further identifies the Cartan grading and is the natural first test case for any technology that must eventually handle larger Clifford algebras or other subalgebras.

Formalizing it. The computation is proved (structurally, by hand, in the research record) but not machine-checked. Everything needed lives in Mathlib: CliffordAlgebra, its $\mathbb{Z}_2$ grading CliffordAlgebra.evenOdd, Submodule, LinearMap, Module.finrank. What the mission produces is a fully verified finite spectral computation inside Clifford algebra — a reusable certificate that the platform's Clifford and grading infrastructure supports exact representation-theoretic bookkeeping, not just algebraic identities.

Difficulty

The obstruction is bookkeeping, not ideas. The natural attack — split indices into active $\{0,2,5\}$ and spectator $\{1,3,4\}$, decompose $\mathrm{Cl}(\text{active}) \otimes \mathrm{Cl}(\text{spectator})$ as a tensor product of graded pieces, and read off the $8 = 2^3$ multiplicity from the spectator sector — requires transferring the $\mathfrak{su}(2)$ action across such a tensor decomposition, which Mathlib does not provide ready-made for Clifford algebras. A purely computational route (fix the 64-element blade basis, build the $32 \times 32$ matrices of the $T_i$ explicitly, compute kernels) is straightforwardly correct but laborious; making it readable is the real work. The statement is stated through arbitrary endomorphisms bound pointwise to the halved adjoint actions precisely so that solvers may choose either route.

Formalization scope

The mission commits to: the quadratic form Q60 as QuadraticMap.weightedSumSquares ℝ (fun _ : Fin 6 => 1); generators e6 i = CliffordAlgebra.ι Q60 (Pi.single i 1); the odd sector as the Mathlib-native CliffordAlgebra.evenOdd Q60 1; and the registered triple as products of two generators. All theorems quantify over endomorphism witnesses bound pointwise to $\tfrac12\,\mathrm{ad}_{E_i}$, so no particular matrix realization is privileged. Spectra are stated as eigenspace decompositions with exact Module.finrank multiplicities — never as pointwise eigenvalue claims, which would be false for mixed vectors. No trivializing formalization exists: the multiplicities are hard constants, and the dimension gate (32) rules out statements about degenerate sector choices. The definition file is reusable for any future mission on $\mathrm{Cl}(6,0)$; the su(2) relations and dimension gate are self-contained milestones. Contributions of either a structural (active/spectator split) or computational (explicit blade basis) proof are equally welcome.

Selected references

• Lawson & Michelsohn, Spin Geometry, Princeton University Press, 1989 (Clifford algebra grading and structure).
• MonumentalSystems, LeanProofs research record #2561 (2026): exact full-sector SU(2) decomposition of $\mathrm{Cl}^-(6,0)$ with multiplicities, https://github.com/MonumentalSystems/LeanProofs
• Mathlib, Mathlib.LinearAlgebra.CliffordAlgebra.Grading (the evenOdd grading used as the odd sector).

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.

Motivation

Waldspurger's non-standard fundamental lemma is an identity between stable orbital integrals on the Lie algebras of two reductive groups that are not isomorphic, and not even isogenous as algebraic groups, but whose root data become identified after tensoring with $\mathbb{Q}$. The basic example is the pair $(\mathrm{Sp}_{2n}, \mathrm{SO}_{2n+1})$, whose root systems $C_n$ and $B_n$ are exchanged by Langlands duality; the identity is what allows the twisted fundamental lemma to be deduced from the ordinary one. Waldspurger formulated the conjecture in L'endoscopie tordue n'est pas si tordue (2008); it is Theorem 1.12.7 of Bao Chau Ngo, Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), proved there in equal characteristic by the same Hitchin-fibration argument that gives the ordinary fundamental lemma.

Before any of that geometry can start, the two sides have to be compared: one needs a single Cartan subalgebra, a single Weyl group and a single space of characteristic polynomials serving both groups at once. Producing that comparison is a self-contained piece of linear algebra over the root data, carried out in Ngo's §1.12, and it is what this mission asks for.

Setting

Let $G_1$ and $G_2$ be split reductive groups over a field, pinned, with maximal tori $T_1$ and $T_2$. Each is determined by its root datum $(X^*(T_i), X_*(T_i), \Phi_i, \Phi_i^\vee, \Delta_i)$, where $\Phi_i$ is the set of roots, $\Phi_i^\vee$ the set of coroots and $\Delta_i$ the set of simple roots singled out by the pinning.

An isogeny of root data between $G_1$ and $G_2$ (Ngo, Definition 1.12.1) is a pair of isomorphisms of $\mathbb{Q}$-vector spaces

$$\psi^* : X^*(T_2)\otimes\mathbb{Q} \longrightarrow X^*(T_1)\otimes\mathbb{Q}, \qquad \psi_* : X_*(T_1)\otimes\mathbb{Q} \longrightarrow X_*(T_2)\otimes\mathbb{Q}$$

which are transposes of one another, such that $\psi^*$ carries the set of lines $\mathbb{Q}\alpha_2$ ($\alpha_2 \in \Phi_2$) bijectively onto the set of lines $\mathbb{Q}\alpha_1$ ($\alpha_1\in\Phi_1$), matching lines of simple roots with lines of simple roots, and such that $\psi_*$ has the same property for the lines spanned by coroots. Two semisimple groups with the same adjoint group are isogenous in this sense; so are a group and its Langlands dual, the interesting cases being $B_n \leftrightarrow C_n$, $F_4$ and $G_2$, where a short root $\alpha$ is sent to $\check\alpha$ and a long root to $n\check\alpha$ with $n = |\alpha_{\mathrm{long}}|^2/|\alpha_{\mathrm{short}}|^2$. Groups obtained by twisting a pair of isogenous pinned groups by a common torsor are called paired.

A prime $p$ is good with respect to $\psi^*$ when it divides neither of the indices

$$\bigl|X_*(T_1)/(X_*(T_1)\cap X_*(T_2))\bigr| \quad\text{and}\quad \bigl|X_*(T_2)/(X_*(T_1)\cap X_*(T_2))\bigr|,$$

the two lattices being compared inside the single $\mathbb{Q}$-vector space identified by $\psi_*$.

Formalization targets

Goal (1.12.4 and 1.12.6): the Weyl groups are identified compatibly

$$\psi_* \, w \, \psi_*^{-1} \in W_2 \quad \text{for all } w \in W_1, \qquad\text{and conversely,}$$

i.e. conjugation by $\psi_*$ carries the Weyl group $W_1$ acting on $X_*(T_1)\otimes\mathbb{Q}$ onto the Weyl group $W_2$ acting on $X_*(T_2)\otimes\mathbb{Q}$. Ngo's reason is that the reflection attached to a root depends only on the line through that root, so the bijection of root lines transports reflections to reflections. This equivariance is what makes the induced isomorphism $\mathfrak{t}_1 \to \mathfrak{t}_2$ descend to an isomorphism $\nu : \mathfrak{c}_{G_1} \to \mathfrak{c}_{G_2}$ of the spaces of characteristic polynomials, which is Lemme 1.12.6 and which is what allows two points $a_1$ and $a_2$ with $\nu(a_1) = a_2$ to be compared at all.

Milestones

Two steps lead there: the reflection computation that makes a matched pair of root lines give a matched pair of reflections, and the integral statement behind Ngo's good-characteristic hypothesis — that when the two indices above are invertible in the base ring, the two lattices become identified after base change.

Significance

Theorem 1.12.7, the non-standard fundamental lemma, asserts that for two paired groups over $O_v = k[[\varpi]]$ with residue characteristic exceeding twice the Coxeter numbers, and for points $a_1$ and $a_2$ corresponding under $\nu$, the stable orbital integrals of the characteristic functions of $\mathfrak{g}_1(O_v)$ and $\mathfrak{g}_2(O_v)$ agree. Waldspurger showed that this identity, together with the ordinary fundamental lemma, implies the twisted fundamental lemma. None of the objects in that statement — reductive group schemes over a discrete valuation ring, orbital integrals, Haar measures on the centralizer tori — exists in Mathlib today. The comparison of §1.12 does not need any of them: it is a statement about lattices, root systems and Weyl groups, and it is a strict prerequisite, since without the isomorphism $\nu$ the two sides of Theorem 1.12.7 cannot even be matched up.

Beyond this paper, the notion of an isogeny of root data and the good-characteristic base change of a pair of lattices are reusable: they are the standard bookkeeping behind Langlands duality for split groups, and neither is currently available.

Difficulty

The reflection step looks like a one-line computation and is one — but only once the two proportionality constants are known to agree. If $\psi^*(\alpha_2) = c\,\alpha_1$ and $\psi_*(\alpha_1^\vee) = c'\,\alpha_2^\vee$, the conjugate of $s_{\alpha_1}$ is $s_{\alpha_2}$ exactly when $c = c'$, and that is forced by transposition together with $\langle\alpha,\alpha^\vee\rangle = 2$. The genuine difficulty in the goal is different: the definition only says that $\psi^*$ and $\psi_*$ permute lines, so one has to show that the bijection induced on root lines and the bijection induced on coroot lines are the same bijection. A solver who assumes this without proof has assumed the substance of 1.12.4.

The lattice milestone has its own trap: the quotient $\Lambda_1/(\Lambda_1\cap\Lambda_2)$ must be shown to have vanishing $\mathrm{Tor}$ after base change, not merely to vanish, or the inclusion becomes only surjective.

Formalization scope

Root data are modelled by Mathlib's RootPairing ι ℚ M N, with $M$ the character space, $N$ the cocharacter space, and rational coefficients throughout, so that "tensoring with $\mathbb{Q}$" is built into the ambient objects rather than performed explicitly. A choice of simple roots is recorded as a subset of the index type rather than as a RootPairing.Base; nothing in the statements depends on that subset beyond its role in the definition of an isogeny. The Weyl group is the subgroup of linear automorphisms of the cocharacter space generated by the coreflections, which is the form in which it acts on the Cartan.

The goal is stated as a two-sided intertwining property rather than as an equality of subgroups: every element of $W_1$ is intertwined by $\psi_*$ with some element of $W_2$ and conversely. This avoids introducing a conjugation homomorphism, and it is the form in which the statement is used. Both root pairings in the goal are required to be finite, reduced root systems, matching Ngo's hypothesis that $G_1$ and $G_2$ are reductive groups.

The good-characteristic condition is formalized exactly as Ngo writes it, by the invertibility in the base ring of the two indices, each expressed as the cardinality of an explicit quotient group; the conclusion is the bijectivity of the map induced on the tensor product by the inclusion of the intersection. If a quotient were infinite its cardinality is reported as $0$, and invertibility of $0$ then forces the base ring to be trivial, so no false statement hides in that corner.

No statement here is vacuous: any pair consisting of a root system and itself, with $\psi^*$ and $\psi_*$ the identity, satisfies every hypothesis, and the pair $(B_n, C_n)$ gives the intended non-trivial instances.

Selected references

• Bao Chau Ngo, Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169. https://doi.org/10.1007/s10240-010-0026-7
• J.-L. Waldspurger, L'endoscopie tordue n'est pas si tordue, Mem. Amer. Math. Soc. 908 (2008). https://doi.org/10.1090/memo/0908
• J.-L. Waldspurger, Le lemme fondamental implique le transfert, Compositio Math. 105 (1997), 153-236. https://doi.org/10.1023/A:1000103112268
• T. A. Springer, Reductive groups, in Automorphic Forms, Representations and L-functions, Proc. Sympos. Pure Math. 33 (1979), 3-27. https://doi.org/10.1090/pspum/033.1

Motivation

Some elementary functions, such as $e^{-x^2}$, $\sin(x)/x$ and $x^x$, have antiderivatives that cannot be written as elementary functions. Liouville's theorem, formulated by Joseph Liouville between 1833 and 1841, is the algebraic statement that explains when an elementary antiderivative can exist: if a function has an elementary antiderivative at all, then that antiderivative lies in the differential field of the function, plus finitely many logarithms. The theorem underlies the Risch algorithm for symbolic integration, which relies on it to find any elementary antiderivative.

Setting

A differential field is a field $F$ together with a derivation $D : F \to F$, i.e. an additive map satisfying $D(ab) = a\,Db + b\,Da$. Its constants form the subfield

$$\operatorname{Con}(F) = \{ f \in F : Df = 0 \}.$$

Let $G \supseteq F$ be a differential field extension (the derivation of $G$ restricts to that of $F$).

• $G$ is a logarithmic extension of $F$ if $G = F(t)$ with $t$ transcendental over $F$ and $Dt = Ds/s$ for some nonzero $s \in F$ (so $t$ behaves like $\log s$).
• $G$ is an exponential extension of $F$ if $G = F(t)$ with $t$ transcendental over $F$ and $Dt/t = Ds$ for some $s \in F$ (so $t$ behaves like $e^{s}$).
• $G$ is an elementary differential extension of $F$ if there is a finite chain of subfields $F = K_0 \subseteq K_1 \subseteq \cdots \subseteq K_m = G$ in which every step $K_{i+1} = K_i(t_i)$ is algebraic, logarithmic or exponential.

The running example is $\mathbb{C}(x)$, the field of rational functions in one variable with the standard derivative $d/dx$.

Formalization targets

Goal: Liouville's theorem

Let $F \subseteq G$ be differential fields of characteristic zero with $\operatorname{Con}(F) = \operatorname{Con}(G)$, and let $G$ be an elementary differential extension of $F$. If $f \in F$ and $g \in G$ satisfy $Dg = f$, then there are $n \ge 0$, constants $c_1, \dots, c_n \in \operatorname{Con}(F)$ and nonzero $f_1, \dots, f_n \in F$, and $s \in F$ with

$$f = c_1 \frac{Df_1}{f_1} + \cdots + c_n \frac{Df_n}{f_n} + Ds.$$

Milestones from the article

1. The constants $\operatorname{Con}(F)$ form a subfield of $F$.
2. $\mathbb{C}(x)$ carries a (unique) derivation extending the formal derivative of polynomials.
3. $\operatorname{Con}(\mathbb{C}(x)) = \mathbb{C}$.
4. $1/x$ has no antiderivative in $\mathbb{C}(x)$.
5. The antiderivatives $\ln x + C$ of $1/x$ exist in the logarithmic extension $\mathbb{C}(x, \ln x)$.
6. $1/(x^2+1)$ has no antiderivative in $\mathbb{C}(x)$.
7. $\displaystyle \frac{1}{x^2+1} = \frac{1}{2i}\,\frac{Du}{u}$ with $u = \frac{1+ix}{1-ix}$, i.e. $\tan^{-1} x = \frac{1}{2i}\ln\frac{1+ix}{1-ix}$ has the form required by the theorem.

Significance

The theorem reduces the question of whether an integral is elementary to a question about the base differential field. That reduction is what makes decision procedures for integration in finite terms (the Risch algorithm) possible, and it is the standard route to proving that $e^{-x^2}$, $\sin(x)/x$ or $x^x$ have no elementary antiderivative.

The result is classical and proved (Liouville; modern algebraic proof by Rosenlicht; textbook proof in Geddes–Czapor–Labahn, §12.4). Mathlib contains a formalization of the algebraic-extension part of the argument (IsLiouville, isLiouville_of_finiteDimensional in Mathlib/FieldTheory/Differential/Liouville.lean); the logarithmic and exponential steps and the full theorem for elementary extensions are the remaining work.

Difficulty

The algebraic steps can be handled by taking traces. The central difficulty is the transcendental steps: for a logarithmic or exponential generator $t$ one must show, by comparing partial-fraction expansions in $t$ and degrees in $t$, that an expression of the Liouville form over $K(t)$ can be pushed down to one over $K$. This needs the hypothesis that no new constants appear. The induction must also track how constants and logarithmic derivatives behave along the whole chain.

Formalization scope

A differential field is a Mathlib Field with a Differential instance (a derivation over $\mathbb{Z}$, written $a'$); the extension $F \subseteq G$ is an Algebra F G with DifferentialAlgebra F G, i.e. $D$ commutes with the embedding. The chain of the elementary extension is a sequence of IntermediateField F G, starting at $\bot$ and ending at $\top$. Each step adjoins a single element, which is algebraic, logarithmic, or exponential over the previous field, and every derivative is computed in $G$. Characteristic zero is assumed (CharZero F). The article does not state it, but it is the standing convention of the theorem in its standard sources. $\operatorname{Con}(F) = \operatorname{Con}(G)$ is stated as the equality of the image of $\operatorname{Con}(F)$ with $\operatorname{Con}(G)$. In the conclusion, the $f_i$ are required to be nonzero, so the quotients $Df_i/f_i$ carry no division-by-zero junk.

For the $\mathbb{C}(x)$ examples, $\mathbb{C}(x)$ is Mathlib's RatFunc ℂ. Mathlib does not provide its derivative, so the examples take an arbitrary derivation satisfying IsStandardDerivation (it agrees with the formal derivative on polynomials). Milestone 2 asserts that exactly one such derivation exists, so the examples are not vacuous.

Selected references

• J. Liouville, Premier / Second mémoire sur la détermination des intégrales dont la valeur est algébrique, J. École Polytechnique XIV (1833), 124–193.
• M. Rosenlicht, Integration in finite terms, Amer. Math. Monthly 79 (1972), 963–972. https://doi.org/10.2307/2318066
• K. O. Geddes, S. R. Czapor, G. Labahn, Algorithms for Computer Algebra, Kluwer, 1992, §12.4.
• Wikipedia, Liouville's theorem (differential algebra), oldid 1349223559.