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.

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.

Motivation

Linear systems are the inner loop of scientific computing: discretized differential equations, least-squares fitting, network flow balances and equilibrium models all end in $Ax = b$. Direct elimination solves the system exactly in $O(n^3)$ operations, but for the large sparse systems produced by discretization the cost and the round-off growth make iterative methods preferable: start from an arbitrary vector and apply a cheap update until the residual is small. The question such a method raises is when the iteration converges, and to that the chapter gives a clean sufficient answer: diagonal dominance.

This mission is the third in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers the iterative part of Chapter 5, Solução de Sistemas Lineares.

Setting

Let $A = (a_{ij})$ be a real $n \\times n$ matrix and $b \\in \\mathbb{R}^n$. Assume $a_{ii} \\neq 0$ for all $i$.

The Jacobi method computes every coordinate of the new iterate from the old one:

The Gauss-Seidel method updates the coordinates in order $i = 1, \\dots, n$ and uses the values already updated in the same sweep:

Both are instances of an affine iteration $x^{(k+1)} = Bx^{(k)} + d$ associated with an equivalent rewriting $Ax = b \\iff x = Bx + d$.

The matrix $A$ is diagonally dominant when each diagonal entry dominates its row:

Target

The goal theorem is Proposição 5.10.1: if $A$ is diagonally dominant and x^\\star solves Ax^\\star = b, then the Gauss-Seidel iterates converge to x^\\star from any starting vector.

The milestones are the general facts the source uses to get there: that the limit of a convergent affine iteration is a fixed point of it and hence a solution of the system (Proposição 5.5.1), that a contraction condition $\\lVert Bv \\rVert \\le c\\lVert v \\rVert$ with $c < 1$ forces convergence to the solution (Proposição 5.5.3), and that the Jacobi sweep has exactly the solutions of $Ax = b$ as its fixed points (Proposição 5.5.2).

Significance

Diagonal dominance is the hypothesis a practitioner can check by inspection, and it is satisfied by the matrices that come from standard finite-difference stencils, from strictly diagonally dominant collocation systems and from many equilibrium models. The theorem says that for those systems Gauss-Seidel needs no spectral analysis and no preconditioner to be safe: convergence holds from any starting vector. The supporting milestones isolate the two halves of the argument — a fixed-point identification and a contraction estimate — in a form reusable for other splittings (Jacobi, SOR, block variants).

Mathlib has Banach's fixed point theorem and the theory of matrix norms, but not the Gauss-Seidel sweep, the notion of diagonal dominance as used here, or the convergence statement, which is what this mission adds.

Difficulty

Gauss-Seidel is not a plain affine map applied coordinatewise: within one sweep the coordinates are updated sequentially, so the new value of coordinate $i$ depends on the new values of coordinates $j < i$. Formalizing the sweep therefore requires a recursion over the coordinate index before the recursion over the iteration counter, and the contraction estimate has to be propagated along that inner recursion. The classical proof compares \\max_i |x_i^{(k+1)} - x_i^\\star| with \\max_i |x_i^{(k)} - x_i^\\star| and needs, for each $i$, a bound that already uses the improved bounds for $j < i$; getting that induction right is the substance of the mission.

Formalization scope

Vectors are functions from a finite index type with $n$ elements to $\\mathbb{R}$, and convergence is convergence in that finite product space (equivalently, coordinatewise). The Gauss-Seidel sweep is defined through an auxiliary partial sweep: after $k$ inner steps the first $k$ coordinates carry their new values and the remaining ones their old values, and the full sweep is the partial sweep after $n$ steps. The Jacobi sweep is defined directly. Diagonal dominance is the strict inequality above, with the sum taken over the row with the diagonal index removed; for $n = 0$ every statement is vacuous, and the goal theorem is then trivially true because the space has a single point. Division by the diagonal entry is total division, so the definitions make sense even when $a_{ii} = 0$; diagonal dominance rules that out, because the right-hand side of the dominance inequality is nonnegative. The goal theorem assumes a solution x^\\star is given rather than asserting its existence, and it asserts convergence for every starting vector, generalizing the source's choice $x^{(0)} = 0$. The contraction milestone states the consistency of the norms as the hypothesis $\\lVert Bv \\rVert \\le c \\lVert v \\rVert$ in the supremum norm rather than fixing a particular matrix norm.

Selected references

• S. R. Freitas, Métodos Numéricos, Departamento de Computação e Estatística, Universidade Federal de Mato Grosso do Sul, 2000. Chapter 5, Solução de Sistemas Lineares, pp. 85–118. (Course notes supplied with this mission.)

Motivation

Invertible modules over a commutative semiring are Zariski-locally free, so local semirings have trivial Picard group. The source asks whether the ring-theoretic semilocal conclusion survives without subtraction: must every invertible module over a semiring with finitely many maximal ideals be free? If not, is the conclusion at least true for finite semirings?

This mission turns CUHK-Shenzhen AI Math Problem 19, Picard groups of semi-local or finite semirings, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

The main theorem asserts freeness for every invertible module over a commutative semiring with finite maximal spectrum. A separate milestone states the finite-semiring fallback. Both are positive formulations; a concrete counterexample to either resolves that target negatively and should motivate a corrected classification.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in semirings, Picard groups, invertible modules, finite semirings. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

Ring proofs use subtraction-sensitive k-ideal properties and decompositions into local factors that can fail for semirings. Finite indecomposable semirings need not be local and may have positive Krull dimension. Invertible modules are projective with strong duality, but familiar rank and determinant arguments may not survive additive noncancellation.

Suggested attack route

Formalize the known local-freeness proof from the evaluation isomorphism and study patching over finitely many principal opens. Identify exactly where partitions of unity require k-ideals. For finite semirings, enumerate idempotent matrices representing projective modules, impose the invertibility constraints, and seek either a reduction to principal rank-one modules or a minimal counterexample. Product decompositions and faithful-action lemmas should be reusable.

Formalization scope

The Lean targets use Mathlib's commutative semiring, maximal spectrum, module, invertible-module, and free-module notions. 'Semilocal' is encoded only as finiteness of MaximalSpectrum; no unproved decomposition theorem is assumed. The finite fallback assumes the underlying semiring type is finite but does not assume the module itself finite separately. Cardinality-only variants from the source are not the capstone.

The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.

Milestones

Resolve the finite-semiring statement, computationally or structurally, while developing the local-to-semilocal patching lemmas needed by the main theorem.

The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on June 24, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

• Original problem
• Facets of Module Theory over Semirings
• MathOverflow discussion

Show that every nonconstant complex polynomial has a complex root.

Motivation

Polynomial equations are the special case of root finding where algebra says a great deal before analysis is needed: the number of roots is known, the roots of a real polynomial come in conjugate pairs, the rational candidates can be listed, and the whole complex plane can be narrowed down to an annulus that must contain every root. A numerical method that exploits this information starts closer to the answer and needs fewer evaluations; and each evaluation itself can be made cheaper by Horner's scheme, which also delivers the deflated quotient for free.

This mission is the second in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 4, Zeros de Polinômios.

Setting

Throughout, a polynomial is written in the book's convention

so the index $i$ names the coefficient of $z^{n-i}$ and $a_0$ is the leading coefficient. The coefficients are real (integral, in the rational-root milestone) and $z$ ranges over $\\mathbb{C}$ unless stated otherwise.

Horner's algorithm computes $P(c)$ by the recurrence $b_0 = a_0$, $b_i = a_i + c\\,b_{i-1}$, so that $P(c) = b_n$, using $n$ multiplications and $n$ additions. The same numbers $b_0, \\dots, b_{n-1}$ are the coefficients of the deflated polynomial $Q$ with $P(w) = (w - c)\\,Q(w) + P(c)$.

With $A = \\max\\{|a_1|, \\dots, |a_n|\\}$ and $B = \\max\\{|a_0|, \\dots, |a_{n-1}|\\}$, the chapter's two localization results confine the roots to the annulus

Target

The goal theorem is the outer bound (Proposição 4.2.1): every complex root of $P$ satisfies $|z| \\le 1 + A/|a_0|$, where $A$ is the largest absolute value among the non-leading coefficients.

The milestones are the companion results of the chapter: the inner bound (Proposição 4.2.2), the fact that non-real roots of a real polynomial occur in conjugate pairs (Proposição 4.1.1), the existence of a real root in odd degree (Proposição 4.1.2), the correctness of Horner's evaluation scheme, and the deflation identity that accompanies it.

Significance

The two localization bounds are what makes a search for complex roots finite: they give an explicit compact region to sweep, and they give scale information that prevents an iteration from wandering off. The conjugate-pair statement halves the work for real polynomials and is the reason odd-degree real polynomials always have a real root. The rational-root test turns exact factorization into a finite search. Horner's scheme is the standard way a polynomial is evaluated inside every root finder, and its deflation identity is what lets a method remove a root that has already been found and continue with a polynomial of lower degree.

Mathlib already contains general results close to some of these (a polynomial over a real closed field of odd degree has a root; rational-root divisibility), so those milestones are accessible; the two localization bounds and the Horner statements in the book's index convention are the substantive new work.

Difficulty

The localization proofs in the source are short but rest on a geometric-series estimate that is only valid for $|z| > 1$; the boundary cases $|z| \\le 1$ have to be treated separately in a formal proof, and the degenerate situations ($n = 1$, coefficients all zero except the leading one) must be checked rather than waved through. The inner bound is obtained from the outer one by the substitution $w = 1/z$, which requires knowing that $z \\neq 0$ is a root of $P$ if and only if $w$ is a root of the reversed polynomial — an argument that has to be made explicit. The Horner statements look computational but need a careful induction because the exponents are natural-number subtractions.

Formalization scope

Coefficients are given as a function $a : \\mathbb{N} \\to \\mathbb{R}$ together with a degree $n$, and the polynomial is the finite sum $\\sum_{i=0}^{n} a_i z^{n-i}$; two versions are provided, one evaluated at a real point and one at a complex point, with the coefficients coerced into $\\mathbb{C}$. Only indices $0 \\le i \\le n$ are read, so the values of $a$ beyond $n$ are irrelevant to every statement. The exponent $n - i$ is natural-number subtraction, which is harmless in this range. No hypothesis says that the family $a$ describes a polynomial of exact degree $n$ beyond the explicit assumptions $a_0 \\neq 0$ or $a_n \\neq 0$ where they appear. The constants $A$ and $B$ are given as hypotheses equating them to the maximum of the relevant finite family of absolute values, rather than being defined separately. The rational-root and odd-degree milestones are stated with Mathlib's polynomial type instead of the coefficient-family encoding, since their statements involve no index convention.

Selected references

• S. R. Freitas, Métodos Numéricos, Departamento de Computação e Estatística, Universidade Federal de Mato Grosso do Sul, 2000. Chapter 4, Zeros de Polinômios, pp. 71–84. (Course notes supplied with this mission.)

Motivation

The most precisely measured property of an elementary particle is the magnetic moment of the electron. The 2022 Northwestern measurement of Fan, Myers, Sukra and Gabrielse (arXiv:2209.13084) reports $-\mu/\mu_B=g/2=1.001\,159\,652\,180\,59\,(13)$, and, combined with the Standard-Model prediction, $\alpha^{-1}=137.035\,999\,166\,(15)$. Those numbers are experimental results, not theorems, and nothing in this mission asserts them.

What is a theorem is the piece of mathematics the measurement rests on. A single electron is held in a Penning trap: a uniform magnetic field plus an electrostatic quadrupole potential. The quantity the experiment needs is the free-space cyclotron frequency $\nu_c=eB/(2\pi m)$, but what a trap lets you observe are its three normal-mode frequencies — the trap-modified cyclotron frequency $\bar\nu_c$, the axial frequency $\bar\nu_z$, and the magnetron frequency $\bar\nu_m$. A real apparatus is never perfect: the magnetic field is tilted relative to the axis of the potential, and the potential is elliptically distorted. The invariance theorem of Brown and Gabrielse (Phys. Rev. A 25, 2423 (1982)), quoted as Eq. (4) of the measurement paper, says that a particular combination of the three observed frequencies is completely insensitive to both imperfections:

This is what makes a part-per-trillion measurement possible with an imperfect trap, and it is the object of this mission.

Setting

Work in $\mathbb{R}^3$. A particle of charge $q$ and mass $m$ sits in a uniform magnetic field $\mathbf B=B\,b$ with $b$ a unit vector, and in the static field of a quadratic electrostatic potential. Dividing the Hessian of that potential by the mass gives a real $3\times3$ matrix $K$, and the equation of motion of the particle is linear:

Two properties of $K$ carry all the physics of the trap: $K$ is symmetric, because it is a Hessian, and traceless, because the potential satisfies Laplace's equation in the vacuum region where the particle moves. Beyond that, $K$ is arbitrary — an arbitrary $K$ is exactly what "the axis of the potential is tilted relative to $b$, and the potential is elliptically distorted" means, so no separate tilt angle or ellipticity parameter appears anywhere.

Substituting the ansatz $r(t)=u\,e^{-i\omega t}$ with $u\in\mathbb{C}^3$ turns the equation of motion into the linear system $M(\omega)\,u=0$, where

is the matrix of $u\mapsto b\times u$. A frequency $\omega$ is a normal mode of the trap precisely when $\det M(\omega)=0$. The three eigenfrequencies of the trap, written $\bar\omega_c,\bar\omega_z,\bar\omega_m$ (angular versions of $\bar\nu_c,\bar\nu_z,\bar\nu_m$), are the non-negative solutions of that equation.

Target

The goal is the invariance theorem in the form: if the three numbers $\bar\omega_c,\bar\omega_z,\bar\omega_m$ are the eigenfrequencies of the trap, in the sense that

then, for every symmetric traceless $K$ and every unit vector $b$,

The milestones are the three steps of the argument, in increasing order of dependence:

1. Mode equation. The exponential ansatz solves the equation of motion at every time if and only if its amplitude lies in the kernel of $M(\omega)$. This is what makes $M(\omega)$ the right object to take determinants of.
2. Characteristic polynomial. For symmetric $K$, $\det M(\omega)$ is real and depends on $\omega$ only through $\omega^2$: it equals $-q(\omega^2)$ with $q(\lambda)=\det(\lambda I-K)-\omega_c^{2}\lambda(\lambda\langle b,b\rangle-\langle b,Kb\rangle)$.
3. Ideal trap. For $K=\operatorname{diag}(-\omega_z^2/2,-\omega_z^2/2,\omega_z^2)$, $b=(0,0,1)$ and $\omega_c^2\ge 2\omega_z^2$, the determinant factors explicitly, with eigenfrequencies $(\omega_c\pm\sqrt{\omega_c^2-2\omega_z^2})/2$ and $\omega_z$.

Significance

The result. The invariance theorem is why the electron magnetic moment can be measured to $0.13$ parts per trillion in an apparatus whose magnetic field and electrode axis are not, and cannot be, exactly aligned. Without it, every misalignment and every elliptic distortion would enter the extracted $\nu_c$ as a systematic error, and the frequency ratio $\nu_a/\nu_c$ that gives $g/2$ would have to be corrected with a model of the imperfections rather than being invariant under them.

Formalizing it. The theorem is a short, completely classical piece of linear algebra — the point of formalizing it is to have the frequency-metrology identity available as a machine-checked statement, together with a reusable model of linear motion in crossed electric and magnetic fields (the mode matrix, its characteristic cubic, and the correspondence between the exponential ansatz and the kernel of the mode matrix).

Status — please read before treating this as open. All four statements in this proposal have been proved by the drafting agent on a local Lean 4.28 / Mathlib installation; the proofs are deliberately not uploaded, so the platform statements are genuinely open here, but this is a formalization-transfer mission, not an open research problem. Milestone 3 is included precisely so that the goal's factorization hypothesis is known to be satisfiable and the goal is not vacuously true. The statements themselves were additionally compiled in this platform's default Lean environment before this proposal was assembled.

Difficulty

The obvious first idea — solve $\det M(\omega)=0$ and add up the roots — is exactly the thing not to do: for a tilted, elliptically distorted trap the three eigenfrequencies have no usable closed form. The whole content of the theorem is that the sum of their squares is the coefficient of $\omega^4$ in the characteristic polynomial and therefore needs no root formula at all: it is Vieta plus the two structural facts $\operatorname{tr}K=0$ and $\langle b,b\rangle=1$. The work in Lean is consequently not analysis but bookkeeping: computing a $3\times3$ determinant with complex off-diagonal entries and extracting one coefficient of the resulting cubic in $\omega^2$. The one place real care is needed is the mode-equation milestone, where derivatives of complex-valued functions of a real variable must be handled honestly.

Formalization scope

Conventions fixed by the Lean statements, and not visible in the prose:

1. Vectors are functions on a three-element index set and matrices are $3\times3$; no abstract inner-product space is used.
2. $K$ is an arbitrary real matrix in the definitions; symmetry and tracelessness are hypotheses on the individual theorems, not part of the model.
3. "Unit vector" is the algebraic condition $\langle b,b\rangle=1$; no norm is used.
4. The magnetic term is $-i\,\omega\,\omega_c\,C(b)$ with $C(b)u=b\times u$, i.e. the sign convention is fixed by the ansatz $r(t)=u\,e^{-i\omega t}$ and the force $\omega_c\,(r'\times b)$.
5. "The eigenfrequencies are $\bar\omega_c,\bar\omega_z,\bar\omega_m$" is formalized as the functional identity $\det M(\omega)=-(\omega^2-\bar\omega_c^2)(\omega^2-\bar\omega_z^2)(\omega^2-\bar\omega_m^2)$ for all real $\omega$ — that is, as a factorization with multiplicity, not as a set of solutions of $\det M(\omega)=0$, which would not pin down multiplicities and would make the sum rule false in degenerate cases.
6. No sign conditions are imposed on $\bar\omega_c,\bar\omega_z,\bar\omega_m$; the conclusion involves only their squares.
7. Nothing in this mission formalizes any measured quantity: $g/2$, $\alpha$, and the frequencies of the actual apparatus appear only as motivation.

Only Mathlib is needed: matrices over $\mathbb{R}$ and $\mathbb{C}$, determinants of $3\times3$ matrices, the cross product, and derivatives of complex-valued functions of a real variable. The definitions are reusable for any linear-motion-in-a-magnetic-field problem.

Selected references

• X. Fan, T. G. Myers, B. A. D. Sukra, G. Gabrielse, Measurement of the Electron Magnetic Moment, Phys. Rev. Lett. 130, 071801 (2023), arXiv:2209.13084 — Eq. (4) is the statement formalized here.
• L. S. Brown, G. Gabrielse, Precision spectroscopy of a charged particle in an imperfect Penning trap, Phys. Rev. A 25, 2423 (1982), doi:10.1103/PhysRevA.25.2423 — the original invariance theorem.
• L. S. Brown, G. Gabrielse, Geonium theory: Physics of a single electron or ion in a Penning trap, Rev. Mod. Phys. 58, 233 (1986), doi:10.1103/RevModPhys.58.233 — the trap eigenfrequencies and the hierarchy $\bar\nu_c\gg\bar\nu_z\gg\bar\nu_m$.

Motivation

In 1982 Yoshio Koide, searching for an empirical formula for the Cabibbo angle, noticed that the three charged-lepton masses satisfy