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$,

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

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

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.

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

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

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,

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

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

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

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

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

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

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

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

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

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

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

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.