Motivation

Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code $C$ over a finite field has a dual code $C^\perp$ consisting of the words orthogonal to all words of $C$ under the standard coordinatewise bilinear form.

The MacWilliams identity states that the full Hamming-weight distribution of $C^\perp$ is determined by that of $C$ through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's The Theory of Error-Correcting Codes. The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.

This development isolates the arbitrary-$q$ Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.

Setting

Let $F$ be a finite field of cardinality $q$, let $\iota$ be a finite coordinate type, and let a word be a function $c:\iota\to F$. A linear code $C$ is an $F$-linear subspace of the word space. The standard bilinear form is

and the dual code is

The Hamming weight $\operatorname{wt}(c)$ is the number of coordinates at which $c$ is nonzero. Writing $n=|\iota|$, the homogeneous Hamming weight enumerator of $C$ is the integer-coefficient polynomial

Thus the coefficient of $X^{n-j}Y^j$ is the number of codewords of weight $j$. The Lean development represents this object symbolically in MvPolynomial (Fin 2) ℤ; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.

Formalization targets

Character orthogonality over a code

For a primitive complex additive character $\psi$ of $F$, define

The first milestone states that $S_C(v)=|C|$ when $v\in C^\perp$ and $S_C(v)=0$ otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.

Coordinatewise Hamming transform

For every word $c$ and all $X,Y\in\mathbb C$, the second milestone records the full character-weighted transform of the Hamming monomial:

This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.

MacWilliams identity

The capstone is the following equality of integer polynomials:

This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula

Significance

The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.

The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.

Difficulty

The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in $\mathbb C$; and the final result is most reusable as an equality of symbolic polynomials over $\mathbb Z$. The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.

The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.

Formalization scope

The coordinate type is an arbitrary finite type rather than only Fin n; its cardinality plays the role of the code length. A word is CodingTheory.Word F ι := ι → F, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.

The polynomial CodingTheory.hammingWeightEnumeratorPolynomial has coefficients in $\mathbb Z$ and variables indexed by Fin 2. Variable $0$ records zero coordinates and variable $1$ records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.

The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to $1=1$. The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.

Selected references

• F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland, 1977, Chapter 5, pp. 125--154; especially Problem 13 (p. 134), Lemmas 9 and 11 (pp. 143--145), and Theorem 13 (p. 146). Publisher chapter record.
• Violetta Weger, Coding Theory, Technical University of Munich lecture notes, 2025, Theorem 11.2 and Lemma 11.8, pp. 154--159.
• F. J. MacWilliams, “A Theorem on the Distribution of Weights in a Systematic Code”, Bell System Technical Journal 42 (1963), 79--94.

Motivation

Around 1637 Pierre de Fermat wrote, in the margin of his copy of Diophantus' Arithmetica, that no $n$-th power with $n > 2$ splits as a sum of two like powers, and that he had a proof the margin was too narrow to hold. The claim resisted every generation of number theorists that attacked it, and the machinery built during those attacks — cyclotomic fields, ideal theory, class numbers, elliptic curves, modular forms, Galois representations — became a large part of modern algebraic number theory. The statement itself is elementary enough to explain to a schoolchild; nothing about its proof is.

Timeline. Fermat himself proved the case $n = 4$ by infinite descent, as a corollary of the fact that the area of a right triangle with integer sides is never a perfect square. Euler treated $n = 3$ in his Vollständige Anleitung zur Algebra (1770), by a descent in $\mathbb{Z}[\sqrt{-3}]$ that assumed a unique-factorization property later supplied by others. Dirichlet and Legendre settled $n = 5$ between 1825 and 1830, Dirichlet added $n = 14$ in 1832, and Lamé published $n = 7$ in 1839. In 1847 Kummer made the decisive structural step: introducing ideal numbers to repair the failure of unique factorization in $\mathbb{Z}[\zeta_p]$, he proved the theorem for every regular prime exponent — those $p$ not dividing the class number of $\mathbb{Q}(\zeta_p)$, a condition he characterized by divisibility of Bernoulli numerators. Irregular primes were left open, and the elementary programme stalled there for over a century.

The route that closed the problem came from a different direction. The modularity conjecture of Taniyama (1955), refined by Shimura and given conceptual support by Weil (1967), predicted that every elliptic curve over $\mathbb{Q}$ arises from a modular form. Hellegouarch and then Frey (1985) attached to a hypothetical solution $a^p + b^p = c^p$ the curve $y^2 = x(x - a^p)(x + b^p)$, whose ramification behaviour is too tame for a curve of its conductor. Serre made this precise as the epsilon conjecture, and Ribet proved it in 1986: modularity of semistable elliptic curves over $\mathbb{Q}$ implies Fermat's Last Theorem. Wiles proved that modularity statement, with the key Hecke-algebra input supplied jointly with Taylor, in two 1995 Annals of Mathematics papers. Breuil, Conrad, Diamond and Taylor removed the semistability hypothesis in 2001.

Setting

Fix a natural number $n$ and natural numbers $a, b, c$. A Fermat triple of exponent $n$ is a triple $(a,b,c)$ of strictly positive naturals with

For $n = 1$ such triples are everywhere, and for $n = 2$ they are the Pythagorean triples, parametrized by $(k(u^2-v^2),\, 2kuv,\, k(u^2+v^2))$. The assertion at issue is that from $n = 3$ upward there are none at all: the hypothesis $3 \le n$ and the positivity hypotheses $0 < a$, $0 < b$, $0 < c$ are exactly what is needed, since $n \le 2$ and the degenerate triples with a zero entry both produce solutions.

Two standard reductions organize any attack. First, if $(a,b,c)$ is a triple of exponent $n$ and $m \mid n$, then $(a^{n/m}, b^{n/m}, c^{n/m})$ is a triple of exponent $m$; since every $n \ge 3$ is divisible by $4$ or by an odd prime $p \ge 3$, the general statement follows from the cases $n = 4$ and $n = p$ an odd prime. Second, for a prime exponent $p$ one may assume $\gcd(a,b,c) = 1$, and the classical literature then splits on whether $p \nmid abc$ (case I) or $p \mid abc$ (case II).

Formalization targets

Goal

This is the mission's single goal, referenced as the published platform theorem fermat_last_theorem. It fixes no exponent, no congruence class, and no auxiliary structure: any complete argument, classical or modern, discharges it.

Significance

The result itself. As a Diophantine statement, Fermat's Last Theorem is a closed case; its value now lies in what proving it required. The proof established the modularity of semistable elliptic curves over $\mathbb{Q}$, made modularity lifting ("$R = T$") a standard technique, and turned Galois deformation theory into a working tool. Those consequences — not the non-existence of Fermat triples — are what the surrounding mathematics uses daily; the Fermat statement is the compact certificate that the machinery works.

Formalizing it. The theorem is proved but not formally verified end to end, and that gap is the mission. Machine-checked proofs exist for the small exponents and for Kummer's regular-prime case: Mathlib carries the general statement together with the cases $n = 3$ and $n = 4$, and the flt-regular project verified the regular-prime theorem in Lean 4. No formal proof of the full theorem exists in any system; Buzzard's ongoing FLT project at Imperial College is building one by reducing the statement to results known to experts by the late 1980s. Contributions here need not follow that route — a complete Lean proof of any single case not yet covered, or of any structural ingredient (level lowering, modularity lifting, the properties of the Frey curve), is a genuine advance, and the platform's sketch mechanism is the natural way to record such a reduction.

Difficulty

The naive attacks fail for identifiable reasons, and a solver should rule them out before spending time on them. Congruence and descent arguments of the kind that settle $n = 3, 4, 5, 7$ depend on the arithmetic of a specific small ring and do not generalize: the descent step needs unique factorization in $\mathbb{Z}[\zeta_n]$ or a substitute, and unique factorization fails there for all but finitely many $n$. Kummer's ideal-theoretic repair recovers the argument exactly when $p$ is regular, and no argument in that family is known to handle irregular primes; the irregular primes are moreover infinite in number, so no finite computation closes them. Parity, size, and modular-arithmetic obstructions have all been shown insufficient, since the equation has solutions modulo every prime power for suitable triples. The only known complete proof passes through modularity, which means the formal development needs elliptic curves over $\mathbb{Q}$, their Galois representations, modular forms and Hecke algebras, level-lowering, and a modularity lifting theorem — none of which is a shortcut around the difficulty, all of which is where the difficulty actually lives.

Formalization scope

The target is stated over $\mathbb{N}$, so no truncated subtraction enters the statement and no sign analysis is hidden in it; the equivalent formulations over $\mathbb{Z}$ and over $\mathbb{Q}$ follow by clearing denominators and moving terms, and a solver who prefers to work over $\mathbb{Z}$ must supply that bridge. Exponentiation is Monoid.npow on $\mathbb{N}$, and $0^0 = 1$ plays no role because $3 \le n$. The hypotheses $0 < a$, $0 < b$, $0 < c$ are all load-bearing and none of them is vacuous, so the statement admits no trivializing reading: dropping any one makes it false, and every hypothesis is satisfiable, so the conclusion cannot be reached by contradiction from the assumptions alone. Mathlib does not contain Fermat's Last Theorem, so the goal cannot be discharged by citing a library lemma.

A complete development will want: the reduction from general $n$ to $n = 4$ and odd prime exponents; the coprimality normalization; cyclotomic fields, class groups, and the regularity criterion for the Kummer line of attack; and, for the modular route, Weierstrass curves over $\mathbb{Q}$, conductors and minimal models, Galois representations attached to torsion points, modular forms and Hecke operators, and the level-lowering and modularity-lifting statements. Most of that infrastructure is reusable well beyond this mission and is welcome as separate published theorems and definitions. Partial contributions are welcome in either style: a direct proof of a single exponent, or a sketch that reduces the goal to child lemmas with statements that stand on their own.

Selected references

• Andrew Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
• Richard Taylor and Andrew Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
• Kenneth A. Ribet, On modular representations of $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476. https://doi.org/10.1007/BF01231195
• Christophe Breuil, Brian Conrad, Fred Diamond and Richard Taylor, On the modularity of elliptic curves over $\mathbb{Q}$: wild 3-adic exercises, Journal of the American Mathematical Society 14 (2001), 843–939. https://doi.org/10.1090/S0894-0347-01-00370-8
• Ernst Eduard Kummer, Beweis des Fermat'schen Satzes der Unmöglichkeit von $x^\lambda + y^\lambda = z^\lambda$ für eine unendliche Anzahl Primzahlen $\lambda$, Monatsberichte der Königlich Preußischen Akademie der Wissenschaften zu Berlin (1847), 132–139.
• Gerhard Frey, Links between stable elliptic curves and certain Diophantine equations, Annales Universitatis Saraviensis 1 (1986), 1–40.
• Riccardo Brasca et al., Fermat's Last Theorem for regular primes (flt-regular), Lean 4 formalization. https://github.com/leanprover-community/flt-regular
• Kevin Buzzard et al., The Fermat's Last Theorem project, Lean 4 formalization in progress. https://imperialcollegelondon.github.io/FLT/

Motivation

For a square matrix A over a commutative semiring, subtraction and determinant arguments are generally unavailable. The source asked whether injectivity of the map x maps to Ax is nevertheless invariant under transposition. The case n=2 was known, with n=3 presented as the first open size.

This mission turns CUHK-Shenzhen AI Math Problem 20, Transpose symmetry for injectivity over 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 capstone states transpose symmetry of function injectivity for every finite matrix size and every unital commutative semiring. In the current Prove2Me snapshot both the general theorem and the dimension-two supporting theorem are published and marked Proved. This mission concerns a resolved result, not an open general declaration. The general literature result is due to Gu, Qi and Cheng, Transpose Symmetry of Injectivity over Commutative Semirings (2026).

Significance

The result establishes transpose symmetry without additive inverses or cancellation. The current formal artifacts already record the finite-dimensional statement over arbitrary unital commutative semirings; users should inspect those exact statements and proof records before selecting extensions. The literature status and formal proof status are both resolved for the linked targets.

Difficulty

Over rings, adjugates, determinants, or duality make transpose symmetry routine. Over semirings, equality of alternating sums cannot be rearranged by subtraction, additive cancellation need not hold, and linear duals do not reflect injectivity. The successful proof must encode parity-separated minors and use injectivity itself to cancel vectors rather than scalars.

Suggested attack route

This mission is historical and solved in the literature. A Prove2Me solution can reconstruct the paper's proof with independently authored Lean code: isolate the even/odd minor algebra, verify the top separation identity, descend through matrix sizes, and derive coefficient equality. Generalizations to nonunital semirings and the parallel surjectivity theorem are natural follow-up nodes, provided their exact hypotheses match the paper.

Formalization scope

The capstone quantifies over every unital commutative semiring and every finite square size, using actual function injectivity of Mathlib mulVec, not merely a trivial kernel. The extra sizes zero, one and two do not weaken the original size-at-least-three question. Both linked theorem items are now Proved on Prove2Me. This update does not copy or redistribute any external repository source, and does not change the published Lean statements or proof identities.

Milestones

The linked dimension-two theorem is Proved. The general goal is also Proved. Any further generalization, such as a nonunital version or a surjectivity statement, would be a separately stated theorem rather than an unfinished part of either existing item.

Timeline and literature status

The source problem was added July 4, 2026. Sixuan Gu, Wei Qi, and Yaoyu Cheng posted a general proof on August 17, 2026, together with a Lean formalization. The mission records that rapid resolution rather than presenting the theorem as currently unknown.

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
• Resolved 2026 paper
• Lean proof repository

Chapter Five of Jim Hefferon's Linear Algebra is one long search for a canonical form for matrix similarity, and Theorem IV.2.8 ends it: over the complex numbers every square matrix is similar to a matrix in Jordan form. That is the goal theorem of this mission and the capstone of the book. Mathlib carries the generalized eigenspace decomposition but has no Jordan canonical form, so this is a genuine target rather than a wrapper around an existing lemma; the Jordan block and the block-diagonal Jordan matrix are supplied as a mission definition. The milestones are the three results the proof is assembled from: diagonalizability as the existence of an eigenbasis, Cayley-Hamilton, and the canonical form of a nilpotent map, which is Jordan form applied to $t - \lambda$ on each generalized eigenspace.

Chapter Three of Jim Hefferon's Linear Algebra is about maps between spaces and how matrices represent them. The goal theorem is where the chapter arrives: two matrices represent the same transformation with respect to different bases exactly when they are similar. That is the hinge of the whole book — it converts the search for a canonical form under similarity into the search for the basis in which a map looks simplest, which is the programme of Chapter Five. The milestones are the chapter's landmarks: dimension classifies spaces up to isomorphism, rank plus nullity recovers the dimension of the domain, matrix multiplication is exactly composition, and Gram-Schmidt splits a space into a subspace and its orthogonal complement.

Chapter Two of Jim Hefferon's Linear Algebra builds the vector space vocabulary — spanning, independence, basis — and turns it into a theory of dimension. The goal theorem is the chapter's most striking result, that the row rank and the column rank of a matrix always agree, which is the bridge between the matrix-of-numbers view of Chapter One and the vector space view of Chapter Two. The milestones are the two pillars it stands on: that any two bases of a space have the same size, so dimension is well defined at all, and that any linearly independent set can be extended to a basis.

Chapter One of Jim Hefferon's Linear Algebra develops Gauss's method and asks what row reduction actually preserves. The answer arrives as the Linear Combination Lemma: row operations change the rows of a matrix but never the subspace those rows span, and that invariant is complete. The goal theorem is that completeness — two matrices are row equivalent exactly when they have the same row space — which is what makes reduced echelon form a genuine canonical form. The milestones are the two results the chapter builds on the way: that row operations leave a system's solution set alone, and that a solution set is always one particular solution translated by the solutions of the associated homogeneous system.

First raised for two variables by Ludwig Kraus in 1884 and stated in full generality by Ott-Heinrich Keller in 1939, the Jacobian conjecture asks something that sounds almost like freshman calculus: if a polynomial map from complex n-space to itself has a Jacobian determinant equal to a nonzero constant, must it be invertible by another polynomial map? That constant-Jacobian condition is precisely the algebraic shadow of the inverse function theorem, yet producing a polynomial — not merely analytic — inverse has resisted every attack for over eighty years. Shreeram Abhyankar championed the problem because it can be stated 'using little beyond a knowledge of calculus,' and Stephen Smale placed it sixteenth on his 1998 list of problems for the new century. Its notoriety is sharpened by a graveyard of published 'proofs' that later collapsed. Deep reductions exist — Bass, Connell, and Wright showed in 1982 that the general case reduces to maps of degree three — and the problem is equivalent, through work of Tsuchimoto, Belov-Kanel, and Kontsevich, to the Dixmier conjecture on the Weyl algebra. A formal statement anchors this famously slippery problem so that progress can be verified rather than merely believed.

Motivation

The exponential function turns addition into multiplication. When its inputs are algebraic numbers, that elementary identity meets a rigid arithmetic boundary: distinct algebraic exponents cannot produce an algebraic linear relation among their exponentials. This principle is the Lindemann–Weierstrass theorem, one of the central results of transcendence theory. Its familiar consequences include the transcendence of Euler's number $e$ and of $\pi$, and therefore the impossibility of squaring the circle with straightedge and compass.

The historical line runs from Hermite's 1873 proof that $e$ is transcendental, through Lindemann's 1882 proof that $\pi$ is transcendental, to Weierstrass's general formulation in 1885. Modern algebraic presentations organize the theorem around conjugates, Galois symmetry, algebraic integers, and an auxiliary-polynomial estimate. The Lean development formalized here follows Yuyang Zhao's mathlib contribution PR #28013, whose mathematical reference is Jacobson's Basic Algebra I, §4.12, Theorem 4.22.

Setting

A complex number is algebraic if it is a root of a nonzero polynomial with rational, equivalently integer, coefficients. A complex number is transcendental if it is not algebraic. Write $\overline{\mathbb Q}\subset\mathbb C$ for the field of algebraic complex numbers and $\exp(z)=e^z$ for the complex exponential.

For a family $(u_i)_{i\in I}$ in $\overline{\mathbb Q}$, injectivity means that distinct indices carry distinct exponents. A family $(x_i)$ is linearly independent over $\overline{\mathbb Q}$ when every finite relation $\sum_i a_i x_i=0$ with algebraic coefficients has all $a_i=0$. It is algebraically independent over $\overline{\mathbb Q}$ when no nonzero multivariate polynomial with algebraic coefficients vanishes on the family.

The strongest target uses natural-number linear independence of $(u_i)$: distinct finitely supported tuples of natural coefficients give distinct sums $\sum_i n_i u_i$. This is exactly the condition needed to distinguish the exponent attached to every monomial.

Formalization targets

Exponential linear independence

For every injective algebraic family $(u_i)$,

This includes the finite Lindemann–Weierstrass relation as its load-bearing finite core.

Hermite–Lindemann and classical constants

For every nonzero algebraic $a\in\mathbb C$,

The same development records the transcendence of $e$, the transcendence of $\pi$, and the transcendence of every nonzero principal logarithm of an algebraic complex number.

Integer winding consumer

Let $\alpha\ne0$ be algebraic and let $w:I\to\mathbb Z$ be injective. The proved Hermite–Lindemann theorem discharges the formerly conditional winding interface and gives

The integer labels are inputs to this arithmetic theorem. A separate topological or dynamical development is responsible for producing them as winding numbers.

Algebraic independence capstone

If $(u_i)$ is a natural-number-linearly-independent family in $\overline{\mathbb Q}$, then

This is the mission's capstone because it turns the linear theorem into a reusable multivariate interface: polynomial monomials become exponentials of distinct natural combinations.

Significance

The theorem separates two kinds of structure that otherwise coexist in the exponential map. The character law $e^{x+y}=e^xe^y$ supplies exact multiplicative relations, but the theorem rules out unintended linear relations over algebraic coefficients. For integer winding consumers, one algebraic nonzero generator $a$ produces the two-sided phase family $(e^{na})_{n\in\mathbb Z}$; after a Laurent-polynomial shift, the theorem makes distinct integer labels linearly independent over $\overline{\mathbb Q}$. Winding supplies the discrete labels, while transcendence supplies arithmetic distinguishability.

The formalization contributes more than the named corollaries. It exposes a finite exponential-relation theorem, the algebraic orbit-sum reduction used by it, and general infinite-family interfaces. These components can be reused in later work on exponential polynomials, logarithms of algebraic numbers, and arithmetic representations of topological charges.

This mission formalizes a known theorem; it is not presented as an open mathematical problem. The private theorem graph is already machine-checked against Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The mission records that proof as an independently inspectable dependency graph before any later upstream integration.

Difficulty

The analytic approximation alone is insufficient. It produces a small complex error, but smallness does not imply vanishing, and taking a field norm does not repair the gap because the other embeddings have no corresponding analytic bound. Likewise, a field automorphism of $\overline{\mathbb Q}$ cannot be moved through the complex exponential as an algebraic operation.

The formal statement therefore requires both an analytic and an arithmetic layer. The arithmetic layer must replace a hypothetical algebraic relation by a Galois-stable relation with integer data and a genuinely nonzero integer contribution. The analytic layer must then make the absolute value of that integer strictly less than one. Managing conjugacy classes, root multisets, denominator clearing, finite supports, and the asymptotic prime choice in one kernel-checked chain is the central formalization difficulty.

Formalization scope

The development is pinned to Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Algebraic complex numbers are represented by integralClosure ℚ ℂ; transcendence corollaries are stated with Transcendental ℤ, which is equivalent to the usual absence of a nonzero integer polynomial relation. The finite theorem uses Fintype; the general linear and algebraic independence theorems permit arbitrary universe-zero index types and reduce relations to finite support internally.

The auxiliary algebraic theorem is stated over an arbitrary algebraically closed field over $\mathbb Q$ and a multiplicative character on its additive group. The analytic consumer specializes this character to the complex exponential. Two small support modules provide quotient lifting for finitely supported functions and evaluation identities for symmetric multivariate polynomials.

The condition $a\ne0$ in Hermite–Lindemann is load-bearing: $e^0=1$ is algebraic. Injectivity of the exponent family is load-bearing for linear independence: duplicate exponents duplicate vectors. The capstone's natural-number linear independence is not algebraic independence of the exponents and must not be silently strengthened or weakened.

The source is an attributed, compatibility-preserving port of the May 2026 Lean 4.30 snapshot of mathlib PR #28013. Platform packaging uses the conservative ASCII rename linearIndependent_exp_finite for the upstream private helper and phi for one Greek binder. The elaborated theorem types were compared against the upstream source; these are naming changes only.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Mathlib contributors, AnalyticalPart: the analytic estimate for Lindemann–Weierstrass. https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.html

Formalize the corrected theory of flavor mixing angles in the su(3) Cartan sector of Cl(6,0), replacing the retired Killing-form/GUT normalization story. The mechanism: T3 and T8 commute, so mixing is carried not by their commutator but by the complete ordered products retained in grade 4. Milestone path: (M1) the grade-4 projection Pi4: Sym^2(A2) -> span{AB,AC,BC} is an isomorphism, with Pi4(e3^2) = -AB, Pi4(e3 e8) = (BC-AC)/sqrt 3, Pi4(e8^2) = (1/3)AB - (2/3)AC - (2/3)BC and tan(2 theta) = sqrt 3 (w-v)/(2u-v-w) for a retained grade-4 field G4 = u AB + v AC + w BC. (M2) the bridge: the primitive finite-T8 Cartan vector Phi = t e3 + e8 with t = sqrt 5 - 2 (the exact r = 16 closure) has grade-4 image exactly the rank-one family tensor phi phi^T; its traceless part is t[[-2,1],[1,2]], the Cabibbo family tensor up to one family-state sign, giving theta_C = arctan(sqrt 5 - 2) ~ 13.28 degrees; the grade-4 tensor has the same Sym2 structure as a left-handed Yukawa Gram operator M M^dagger. (M3, guarded goal) identify the r = 16 tensor with the relative left-family Yukawa tensor, closing the Sym2/Gram bridge. Foundational lemmas (A2 Cartan plane with [T3,T8] = 0, the complete 7-bracket su(3) table, grade-4 square residuals, grade-6 cubic channel) are landed in the LeanProofs repository and will be contributed as importable platform nodes ahead of the milestones. Recorded provenance: HAM memories #2848 (FullGradeCartanMixingTensorV1, 2026-09-14) and #3099 (CabibboGramSym2BridgeV1, 2026-09-17), proof DAG galaxy.proof-dag.v1 grade4-cartan-mixing.

Motivation

The fundamental lemma is a family of identities between orbital integrals on a reductive group and stable orbital integrals on a smaller group attached to it, its endoscopic group. Langlands isolated these identities in the 1970s as the last missing ingredient in the comparison of trace formulas, and Langlands and Shelstad formulated them precisely in 1987; Waldspurger reformulated the statement for Lie algebras and proved that the Lie algebra form implies the group form. The Lie algebra statement was proved in equal characteristic by Bao Chau Ngo in Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), by a global geometric argument built on the Hitchin fibration; Waldspurger's earlier work transfers the result to mixed characteristic. The identity is the engine behind the stabilization of the trace formula and behind the computation of the cohomology of Shimura varieties.

Both sides of the identity carry a normalizing factor built from the discriminant, and the exact power of $q$ relating the two normalizations is fixed by a purely root-theoretic computation carried out in Ngo's §1.10-§1.11. That computation is the subject of this mission. It is self-contained, it uses no geometry, and it is the first piece of the paper that can be stated in Lean today.

Setting

Let $G$ be a split reductive group over a field with maximal torus $T$, character lattice $X^*(T)$, cocharacter lattice $X_*(T)$, root system $\Phi \subset X^*(T)$ and Weyl group $W$. Write $\mathfrak{t}$ for the Cartan subalgebra, so that each root $\alpha$ has a differential $d\alpha$, a linear form on $\mathfrak{t}$. Ngô's discriminant is the product

a $W$-invariant polynomial function on $\mathfrak{t}$ and hence a function on the space $\mathfrak{c} = \mathfrak{t} /\!/ W$ of characteristic polynomials.

An endoscopic datum is an element $\kappa$ of the dual torus $\hat{T} = \operatorname{Hom}(X_*(T), \mathbb{G}_m)$. The endoscopic group $H$ attached to it is the group whose root system is

with Weyl group $W_H \subset W$ and its own discriminant $D_H = \prod_{\alpha \in \Phi_H} d\alpha$. Choose a subset $\Lambda \subset \Phi - \Phi_H$ containing exactly one root out of each pair $\{\alpha, -\alpha\}$ of opposite roots outside $\Phi_H$, and set

Finally let $F$ be a non-archimedean local field with valuation $v$ and residue cardinality $q$, and recall Ngô's normalizing factors $\Delta_G(a) = q^{-v(D_G(a))/2}$ and $\Delta_H(a_H) = q^{-v(D_H(a_H))/2}$.

Formalization targets

Goal (1.11.3): the transfer factor identity

for a point $a_H$ of the endoscopic Cartan with image $a$. Equivalently $\Delta_H(a_H)\Delta_G(a)^{-1} = q^{\,r}$ with $r = v(R^G_H(a_H))$: this is exactly what lets one pass between the two forms of the fundamental lemma, $O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}) = q^{\,r} SO_{a_H}(\mathbf{1}_{\mathfrak{h}})$ and $\Delta_G(a) O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}) = \Delta_H(a_H) SO_{a_H}(\mathbf{1}_{\mathfrak{h}})$.

Milestones

The identity above is the image under $v$ of the divisor identity $\nu^* D_G = D_H + 2 R^G_H$ of 1.10.3, which in turn rests on the fact that $R^G_H$ — which depends on a choice of $\Lambda$ — is nevertheless $W_H$-invariant, and on the fact that $\Phi_H$ really is a root subsystem. The milestone list follows that order.

Significance

Theorem 1 of Ngô's paper, the Langlands-Shelstad conjecture for Lie algebras, is the identity $\Delta_G(a) O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}, dt) = \Delta_H(a_H) SO_{a_H}(\mathbf{1}_{\mathfrak{h}}, dt)$ for corresponding regular semisimple stable classes, under the hypothesis that twice the Coxeter number of $G$ is smaller than the residue characteristic. Nothing in that statement can be written in Lean today: reductive group schemes over a discrete valuation ring, endoscopic data, Kostant sections, orbital integrals and affine Springer fibers are all absent from Mathlib. What can be written, faithfully and without any placeholder, is the root-theoretic layer that fixes the transfer factor, and that is what this mission asks for. It is a genuine prerequisite: the two displayed forms of Theorem 1 differ precisely by the identity above.

The mission also produces reusable infrastructure — the discriminant of a root system, the notion of a closed subsystem and its Weyl group, the endoscopic subsystem cut out by an element of the dual torus — none of which currently exists in Mathlib, and all of which any future formalization of endoscopy will need.

Difficulty

Only one of the four milestones is a routine manipulation. Splitting $\Phi - \Phi_H$ into pairs $\{\alpha,-\alpha\}$ and collecting squares is bookkeeping; that $D_G$ is $W$-invariant is immediate because $W$ permutes $\Phi$. The content is in Lemma 1.10.2: $\Lambda$ is not stable under $W_H$, so $w \in W_H$ carries $\prod_{\alpha\in\Lambda} d\alpha$ to $(-1)^{m(w)} \prod_{\alpha\in\Lambda} d\alpha$, where $m(w)$ counts the roots of $\Lambda$ sent into $-\Lambda$; the claim is that $m(w)$ is always even. The naive attempt — check it on the generating reflections of $W_H$ — is exactly where a careless argument goes wrong, since it is false for reflections in roots outside $\Phi_H$. Ngô's argument identifies the sign with $(-1)^{\ell_G(w)} (-1)^{\ell_H(w)}$, the ratio of the sign characters of $W$ and $W_H$, and observes that both compute the determinant of $w$ acting on the same reflection representation.

Formalization scope

Root systems are modelled with Mathlib's RootPairing ι R M N: the module $M$ plays the role of $X^*(T)$, the module $N$ the role of $X_*(T)$ and of the Cartan on which the differentials $d\alpha$ are evaluated, and $P.root' i$ is the linear form $d\alpha$. The endoscopic subsystem is cut out by an element $\kappa$ of the dual torus, taken as a group homomorphism from the cocharacter lattice to an arbitrary commutative group, and is expressed over $\mathbb{Z}$ coefficients as in the definition of a root datum. Products over $\Phi$ and $\Phi_H$ are finite products over a Fintype index, and a choice $\Lambda$ is a Finset satisfying an exclusive-or condition, which automatically rules out the degenerate case $\alpha = -\alpha$.

The identity 1.10.3 is stated as an identity of functions on the Cartan rather than as an identity of divisors, so the unit $(-1)^{|\Lambda|}$ is carried explicitly rather than discarded. Lemma 1.10.2 is stated over $\mathbb{Q}$ for an honest root system, since the sign argument uses the reflection representation. The goal 1.11.3 is stated for an additive valuation with values in $\mathbb{Z} \cup \{\infty\}$, which is what makes the two sides comparable when a discriminant vanishes.

There is no trivializing formalization here: the hypotheses of every item are satisfiable — any root system with any closed subsystem and any choice of $\Lambda$ gives an instance — so none of the statements is vacuous, and none of them is an identity between two occurrences of the same expression.

Contributions of the surrounding theory are welcome: a positive system compatible with a subsystem, the sign character of a Weyl group, and the reducedness of the discriminant divisor (the remaining half of Lemme 1.10.1) are all natural next steps.

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
• R. Langlands, D. Shelstad, On the definition of transfer factors, Math. Ann. 278 (1987), 219-271. https://doi.org/10.1007/BF01458070
• J.-L. Waldspurger, Endoscopie et changement de caracteristique, J. Inst. Math. Jussieu 5 (2006), 423-525. https://doi.org/10.1017/S1474748006000041
• R. Kottwitz, Transfer factors for Lie algebras, Represent. Theory 3 (1999), 127-138. https://doi.org/10.1090/S1088-4165-99-00077-6
• T. Hales, A statement of the fundamental lemma, in Harmonic Analysis, the Trace Formula, and Shimura Varieties, Clay Math. Proc. 4 (2005), 643-658. https://arxiv.org/abs/math/0312227

Motivation

Classical Eilenberg correspondence theorems connect algebraic descriptions of finite-state behavior with language-theoretic closure principles. The version developed by Juan Climent Vidal and Enric Cosme Llópez replaces one-sorted monoids by many-sorted algebras, so that operations may accept arguments of several prescribed sorts and return a value of another sort. This is the natural algebraic setting for typed term languages: a signature records the permitted input and output sorts of each operation, and a language is a family of sets indexed by sorts. The paper proves that two ways of organizing finite-state behavior—through finite-index congruences and through regular languages—determine the same ordered structure. The source is the final section of Climent Vidal and Cosme Llópez, Eilenberg theorems for many-sorted formations, published in the Houston Journal of Mathematics 45(2), 2019.

The companion manuscript A Kleene theorem for free many-sorted algebras develops the free-term and recognizability infrastructure used by this formalization. It supplies a concrete Lean representation of sorted signatures, free algebras, homomorphisms, terms, and finite many-sorted carriers. The present mission begins from that reusable core and formalizes the formation-level theorem of the HJM paper, rather than repeating the already completed Kleene development.

Setting

Fix a finite type of sorts $S$ and an $S$-sorted signature $\Sigma$. For an $S$-sorted set $X$, write $T_\Sigma(X)$ for the free $\Sigma$-algebra on $X$. A congruence $\Phi$ on a many-sorted algebra is a family of equivalence relations $\Phi_s$, one on each carrier sort, compatible with every basic operation. Its index is finite when the entire sorted quotient family

is finite. A sorted language $L$ is $\Phi$-saturated when membership in $L_s$ is constant on every $\Phi_s$-class. The syntactic congruence $\Omega(L)$ is the greatest algebra congruence that saturates $L$, and $L$ is regular when $\Omega(L)$ has finite index.

A finite-index congruence formation $\mathfrak F$ selects, for every variable family $X$, a nonempty filter $\mathfrak F(X)$ of finite-index congruences on $T_\Sigma(X)$. The selection is closed under intersections, upward inclusion, and pullback along homomorphisms whose composite with the relevant quotient projection is surjective at every sort.

A regular-language formation $\mathcal L$ selects regular languages in each $T_\Sigma(X)$. It contains every language saturated by the universal congruence; whenever $L,K\in\mathcal L(X)$ it contains every language saturated by $\Omega(L)\cap\Omega(K)$; and it satisfies the corresponding pullback-saturation condition for quotient-surjective homomorphisms.

The two constructions are

and

Formalization targets

The capstone is the paper's final formation theorem: the ordered sets of finite-index congruence formations and regular-language formations are order-isomorphic, with the isomorphism fixed to be exactly the two displayed constructions.

The milestones establish the universal property of the syntactic congruence, closure of finite-index congruences under the filter operations, the well-definedness of each construction, and the two recovery identities

These identities determine the inverse maps and prevent the goal from being satisfied by an unrelated abstract order equivalence.

Significance

The theorem packages a family of finite quotients and a family of regular languages as interchangeable data. On the algebraic side, closure is expressed by filters of congruences and quotient-surjective pullbacks. On the language side, the same information is expressed through saturation by syntactic congruences. The result therefore gives a systematic translation between quotient-based and language-based classifications in a typed, many-sorted setting.

Formalizing the theorem adds congruence, quotient-index, saturation, syntactic-congruence, and formation interfaces to the existing free many-sorted algebra library. These components are reusable for future formalizations of recognizability, Myhill–Nerode principles, finite algebra formations, and varieties or pseudovarieties of typed algebras. The mathematical theorem is already proved in the cited 2019 paper; the remaining task is to produce machine-checked Lean proofs of the source-faithful statements.

Difficulty

The two maps are simple to write down but their inverse laws are not pointwise tautologies. A finite-index congruence must be reconstructed from the family of all languages it saturates, and a language formation must be reconstructed from all selected finite-index congruences. In the many-sorted case, finiteness applies to the entire quotient family, including its support across sorts, and intersections and pullbacks must preserve this global condition. The quotient-surjectivity premise is also essential: replacing it by ordinary surjectivity of the original homomorphism would change the formation axiom.

The syntactic congruence creates a second layer of care. It must be characterized as the greatest compatible sorted equivalence saturating a language, not merely as the kernel of the language's characteristic function, which need not itself respect the algebra operations. Thus an argument that treats saturation as an arbitrary set-theoretic equivalence misses the algebraic compatibility required by the theorem.

Formalization scope

The Lean development uses the existing MSKleene representation of sorted sets, signatures, argument tuples, algebras, homomorphisms, terms, and free algebras. Congruences are sort-indexed setoids with explicit compatibility for every signature operation. Their order is inclusion of relations. Intersection and the universal congruence are concrete constructions, while pullback is defined along an algebra homomorphism.

Finite index is represented by finiteness of the sigma-type of all quotient carriers, matching the paper's finite sorted-set convention; it is not weakened to separate finiteness of each inhabited component. The sort type is assumed finite in the finite-index filter and formation correspondence theorems, as required in the final section of the source. Languages are arbitrary sorted subsets of free term algebras, including empty components. No nonemptiness assumption on variable carriers or algebra sorts is added.

The syntactic congruence is defined internally as the supremum-style least upper bound of all congruences saturating a language, rather than postulated together with its universal property. The formation structures contain only the source closure axioms. In particular, neither correspondence map nor either inverse identity is stored as a structure field; doing so would trivialize the capstone. Contributions are welcome on the foundational universal-property and finite-index lemmas, the two formation constructors, and the recovery identities that assemble into the final order isomorphism.

Selected references

• Juan Climent Vidal and Enric Cosme Llópez, Eilenberg theorems for many-sorted formations, Houston Journal of Mathematics 45(2), 2019, pp. 351–416. arXiv:1604.04792
• Samuel Eilenberg, Automata, Languages, and Machines, Volume B, Academic Press, 1976.
• Adolfo Ballester-Bolinches, Jean-Éric Pin, and Xaro Soler-Escrivà, Formations of finite monoids and formal languages: Eilenberg's variety theorem revisited, Forum Mathematicum 26, 2014, pp. 1737–1761.

Motivation

Kleene's theorem (Kleene 1956; McNaughton–Yamada 1960) is a cornerstone of formal language theory: over a free monoid, the languages recognized by finite automata are exactly the regular ones — those built from finite languages by union, concatenation, and the Kleene star. Mezei and Wright (1967) lifted recognizability off strings, calling a subset of an arbitrary algebra recognizable when it is the preimage of a subset of a finite algebra under a homomorphism. Replacing strings by terms — finite trees labelled by operation symbols — gives the theory of recognizable tree languages and finite tree automata of Gécseg and Steinby (1984), where the Kleene correspondence reappears with a tree concatenation and an iteration operation in the role of the star.

Many computational structures are inherently many-sorted: typed lambda calculi, structured programming languages, process calculi, XML schemas — data and operations organized into distinct sorts. In the many-sorted setting a signature assigns to each operation symbol the sorts of its arguments and of its value, variables carry sorts, and a language is a sort-indexed family of term sets. The predecessor of this mission, Climent Vidal–Cosme Llópez 2020 (CVCL20), established that recognizability over free many-sorted algebras is preserved — and, where applicable, reflected — by substitution, iteration, quotient, inverse tree-homomorphic image, and direct linear image, via finite-index congruences. What CVCL20 left open is the regular side: whether a natural class of many-sorted regular expressions captures exactly the recognizable languages. This mission closes that gap.

Setting

Fix a finite set of sorts $S$. An $S$-sorted set $A = (A_s)_{s\in S}$ is a family of sets; it is finite when $\coprod_{s\in S} A_s$ is finite. An $S$-sorted signature $\Sigma$ assigns to each pair $(\mathbf{s}, s) \in S^\star \times S$ a set $\Sigma_{\mathbf{s},s}$ of operation symbols of arity $\mathbf{s}$ and coarity $s$. A $\Sigma$-algebra $\mathbf{A}$ is an $S$-sorted set $A$ together with, for each $\sigma \in \Sigma_{\mathbf{s},s}$, an operation $\sigma^{\mathbf A}\colon A_{\mathbf s} \to A_s$, where $A_{\mathbf s} = \prod_{j} A_{s_j}$. A homomorphism commutes with all operations sortwise.

The free $\Sigma$-algebra $\mathbf T_\Sigma(X)$ on an $S$-sorted set $X$ of variables has as its sort-$s$ carrier $\mathrm T_\Sigma(X)_s$ the set of $(X,s)$-terms; every $S$-sorted map $X \to A$ extends uniquely to a homomorphism $\mathbf T_\Sigma(X) \to \mathbf A$. Following automata-theoretic tradition, subsets of $\mathrm T_\Sigma(X)$ are called languages. For a sort $s$, a language $L \subseteq \mathrm T_\Sigma(X)_s$ is $s$-recognizable when there are a finite $\Sigma$-algebra $\mathbf N$, a homomorphism $f\colon \mathbf T_\Sigma(X) \to \mathbf N$, and a subset $M \subseteq N_s$ with $L = f_s^{-1}[M]$. Write $\mathrm{Rec}_s(\mathbf T_\Sigma(X))$ for the set of all such $L$.

Two operations on languages, both performed sortwise, generate the regular expressions. Given a variable $z \in X_u$ and a language $L \subseteq \mathrm T_\Sigma(X)_u$, $z$-substitution $\left(\!\begin{smallmatrix}z\\ L\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s$ replaces, in every term of an input language of sort $s$, each occurrence of $z$ independently by a term of $L$. The $z$-iteration is $L^{\star z} = \bigcup_{i\in\mathbb N} L^{i\,z}$, where $L^{0\,z} = \{z\}$ and $L^{i+1\,z} = L^{i\,z} \cup \left(\!\begin{smallmatrix}z\\ L^{i\,z}\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s(L)$. For a finite $S$-sorted set $Z$, the regular signature $\mathrm{Reg}(S,\Sigma,Z)$ expands $\Sigma$ by an empty constant $\varnothing_s$, a binary sum $+_s$, a unary $z$-iteration $(\cdot)^{\star z}$ for each $z\in Z_s$, and a $z$-substitution operation for each $z\in Z_t$. Its terms are the regular expressions over $(S,\Sigma,Z)$; the power algebra $\mathbf T_\Sigma(Z)^\wp$ carries a canonical $\mathrm{Reg}(S,\Sigma,Z)$-algebra structure, and interpreting a regular expression there yields a language $\{R\}^{Z\sharp}_s$. A language $L\subseteq \mathrm T_\Sigma(X)_s$ is $s$-regular when $L = \{R\}^{Z\sharp}_s$ for some finite $Z\supseteq X$ and some regular expression $R$ of type $s$; write $\mathrm{Reg}_s(\mathbf T_\Sigma(X))$.

Formalization targets

Goal — the many-sorted Kleene theorem

The statement fixes no automaton model and no normal form for regular expressions: it asserts only that the two classes of languages coincide, at every sort, for every finite $S$, every finite $S$-sorted signature $\Sigma$, and every finite $S$-sorted set $X$. It splits into $\mathrm{Reg}_s \subseteq \mathrm{Rec}_s$ (Corollary 4.8) and $\mathrm{Rec}_s \subseteq \mathrm{Reg}_s$ (Proposition 4.10).

Significance

The result completes the Kleene–Myhill–Nerode correspondence on the side of universal algebra, uniformly over an arbitrary finite many-sorted signature: it names the exact operations — those of $\Sigma$, plus empty language, union, sortwise substitution, and sortwise iteration — that generate precisely the finite-state behaviours. Over non-free structures the correspondence is known to fail (recognizable but non-rational subsets of a monoid, Eilenberg 1974), which is what makes the free many-sorted algebra the natural home for an exact statement. The forward direction organizes the regular languages into a $\mathrm{Reg}$-algebra and instantiates the closure properties of CVCL20; the converse gives a constructive, syntactic procedure — from a recognizing homomorphism it builds a regular expression denoting the language — generalizing Lemma 2.5.7 of Gécseg–Steinby, itself descended from McNaughton–Yamada.

The paper is new (June 2026) and has no machine-checked proof. This mission produces the first formalization: a reusable Lean development of finite many-sorted universal algebra — signatures, algebras, free term algebras and their universal property, the Artinian subterm order, power algebras, recognizability, and the substitution/iteration calculus — together with the two inclusions and the state-elimination argument. Everything below the §4 headline results is infrastructure of independent value for many-sorted formal language theory.

Difficulty

The converse inclusion is the substance. The single-sorted proof eliminates automaton states one at a time along a single axis; the naive port to the many-sorted case — fix a linear order on all states and eliminate — loses track of the sort at which each elimination happens and does not terminate cleanly. The argument instead carries a sortwise budget: an $S$-sorted family $K \le N$ recording, for each sort $t$, the set $K_t$ of state values still admissible at internal subterms. The induction is on $\lVert\lVert K\rVert\rVert = \sum_{s\in S} k_s$, and each step removes the top state of one chosen sort, so the recursion branches over the sorts whose budget is nonzero and the key identity (Equation (E)) is a union over those sorts. The inductive invariant — the family of auxiliary languages $L_u(C,K,l)$ with its budget bookkeeping — is what separates the many-sorted argument from its ancestor; it is also the part Gécseg–Steinby declare "obvious from the construction" and this proof spells out in full (Claims C1–C6).

Formalization scope

Proposed Lean representation: $S$ a type with [Fintype S]; an $S$-sorted set as S → Type; a signature as a family List S → S → Type with finiteness where the theorems need it; the free algebra as an inductive term type; the power algebra with sort-$s$ carrier Set (T_Σ Z s); $s$-recognizability as the existence of a finite $\Sigma$-algebra, a homomorphism, and a subset whose sortwise preimage is the language. Committed conventions: $S$ finite throughout; $\Sigma$ finite and $X$ finite for the §4 results (so that only finitely many basic terms exist and the budget induction is well-founded); the regular operations are exactly $\{\varnothing, +, (\cdot)^{\star z}, z\text{-subst}\}$ together with the operations of $\Sigma$ — not an unrestricted Boolean or closure algebra, which would trivialize the statement.

A complete development needs: the many-sorted UA core (sorted sets and maps, signature, algebra, homomorphism, subalgebra, congruence); the free algebra with unique readability (Proposition 3.4) and universal property (Proposition 3.5); the Artinian subterm order (Proposition 3.6); the power algebra; recognizability and $s$-recognizability with the CVCL20 closure results (Propositions 3.29, 3.30, 3.33); the substitution and iteration calculus (Lemmas 3.23, 3.25, 3.28, Corollary 3.17, Lemma 3.18); and the §4 regular-expression layer (Definition 4.1, Proposition 4.3, Corollary 4.4, Definition 4.6). The UA core and the substitution calculus are reusable beyond this mission. Contributions are welcome at every level — the definitions, the closure results, the auxiliary claims C1–C6, and either inclusion.

Selected references

• L. Gong, R. Ruiz Mora, N. Sanmartín Vich, E. Cosme Llópez, A Kleene theorem for free many-sorted algebras, 2026.
• J. Climent Vidal, E. Cosme Llópez, Congruence-based proofs of the recognizability theorems for free many-sorted algebras, Journal of Logic and Computation 30(2) (2020), 561–633. https://arxiv.org/abs/1808.08217
• F. Gécseg, M. Steinby, Tree Automata, Akadémiai Kiadó, Budapest, 1984.
• R. McNaughton, H. Yamada, Regular expressions and state graphs for automata, IRE Transactions on Electronic Computers EC-9 (1960), 39–47.
• S. C. Kleene, Representation of events in nerve nets and finite automata, in Automata Studies, Princeton University Press, 1956, 3–42.
• J. Mezei, J. Wright, Algebraic automata and context-free sets, Information and Control 11 (1967), 3–29.
• S. Eilenberg, Automata, Languages, and Machines, Vol. A, Academic Press, New York, 1974.

Arithmetic relations among elliptic-function values

Formalization status, 29 September 2026: the main theorem and all nine linked milestones are Proved, with zero Open leaves. The selected proof uses the now-Proved Philippon Theorem 2.1 and the completed Weierstrass application bridges. The linked statements retain their explicit formalization conventions and intermediate variants.

Algebraic independence measures whether several complex numbers satisfy a polynomial relation with rational coefficients. For two numbers, independence means that no nonzero polynomial in two variables vanishes at that pair. This is stronger than asking that each number separately be transcendental: two transcendental numbers can still satisfy a polynomial relation with each other. The distinction matters when describing the arithmetic information carried jointly by periods, lattice invariants, and values of analytic functions.

The completed target is Theorem 1 of Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions (2026). It concerns ten numbers attached to a complex lattice and two evaluation points. The conclusion selects an algebraically independent pair from those ten entries; it does not specify that the pair must consist of two particular function values. The mathematical result is published, and this mission now supplies its checked Lean proof. A source comparison on 29 September 2026 checked the main theorem’s hypotheses, ten values, full-period quasi-period normalization and pair-independence conclusion. The main statement needs no correction.

A lattice and its canonical functions

Take complex numbers $\omega_1,\omega_2$ that are linearly independent over the real numbers. Their integer linear combinations form the period lattice

The formal representation is Mathlib's PeriodPair. Its lattice determines the Weierstrass elliptic function $\wp$ and invariants $g_2,g_3$, using Mathlib's existing definitions. Thus the lattice, function, and invariants are linked by their construction; they are not unrelated parameters.

The Weierstrass zeta function is fixed by the lattice series

This is the normalization in DLMF equation 23.2.5. For a lattice element $\omega$, its quasi-period is represented by

Both arguments lie outside the lattice. Relating this fixed increment to the increment at an arbitrary regular point is part of the established analytic infrastructure. The normalization concerns the full period $\omega$; references using half-periods require the corresponding factors of two, as in DLMF equation 23.2.11.

Formalization targets

Theorem 1: an algebraically independent pair

Let $\omega\ne0$ belong to $\Omega$. Suppose $u_1,u_2,\omega$ are linearly independent over $\mathbb Q$ and

Define the indexed tuple

The proved conclusion is

These are the hypotheses and conclusion of the paper's Theorem 1. No algebraicity assumption is imposed on $g_2$ or $g_3$, and the conclusion does not assert independence of all ten entries.

Equations (5) and (6): supporting addition identities

The initial supporting targets are the two identities used in §4 of the paper. For $z,v,z+v\notin\Omega$, write $\Delta=\wp(v)-\wp(z)$. They assert

and

The statements preserve the paper's multiplied-out forms. They do not require $\Delta\ne0$. These targets supply reusable identities; proving them alone does not establish the arithmetic conclusion of Theorem 1.

Nine completed milestones

The grid and degree variants are described in the linked statements. The two application bridges identify the Weierstrass objects with the general group-theoretic objects used by Philippon’s theorem.

What the completed formalization establishes

The completed goal certifies that every period pair and every triple satisfying the stated hypotheses yields an independent pair in the precise ten-entry tuple. In particular, a proof must handle arbitrary complex lattice invariants and arbitrary admissible evaluation points. A result for a preferred lattice, algebraic arguments, or a predetermined choice of indices would leave the requested statement unresolved.

The definitions provide a reusable interface for elliptic zeta values: a canonical series, a fixed quasi-period convention, and an explicit finite-family independence predicate. The main theorem and all nine milestones have checked proofs; the theorem pages record their accepted submissions and dependencies.

Analytic identities and arithmetic independence

The central difficulty in the proof is passing from identities of analytic functions to exclusion of rational polynomial relations among selected complex values. Periodicity and the addition identities describe how values are related, but do not by themselves rule out algebraic dependence. Consequently, finishing the elementary function interface is only one part of the development.

The development also addresses a concrete analytic obligation in the chosen representation. An infinite-sum expression is a total Lean term even before summability is proved. Using it as the canonical analytic zeta function requires the appropriate convergence and differentiation results. The classical convergence statement is recorded in DLMF §23.2(ii); it is not introduced as an extra hypothesis of the main theorem.

Formalization scope and conventions

All custom declarations use the namespace WeierstrassEllipticZeta. The lattice intersection is an equality of $\mathbb Z$-submodules of $\mathbb C$. Rational linear independence and real linear independence have different roles: the first constrains the three inputs to the theorem, while the second is built into the period pair. Neither is replaced by numerical noncollinearity checks or approximate arithmetic.

The ten values form a Fin 10 family. The selected pair uses Mathlib's AlgebraicIndependent over $\mathbb Q$, so repeated numerical values cannot supply an independent pair merely by occupying different indices. The existing assumptions imply that both evaluation points are outside the lattice; no extra exclusion hypothesis is needed for the goal. Supporting addition identities state their pole exclusions explicitly because Lean's totalized division also assigns values at zero denominators.

The linked intermediate targets identify the variants sufficient for the completed main proof: Lemma 8 uses the stated formal-grid formulation; Proposition A.1 concerns the mission’s rank-one grid; and Lemma 10 uses linear coordinate-degree bounds rather than the source’s sharper O(N/log N) bounds. These distinctions are explicit in the milestone statements. They do not add assumptions to the main theorem. Further contributions can simplify the checked proofs, improve these intermediate bounds, or extend the general results beyond the existing mission target.

Extensions beyond the paper

Theorem 1 with only individual pole exclusions is an Open follow-up target. It retains the same nonzero period, rational linear independence, and ten-entry algebraic-independence conclusion, while replacing the lattice-intersection hypothesis with $u_1,u_2\notin\Omega$.

This extension is an additional deduction to formalize, not a numbered result of the paper, and no mathematical novelty is claimed. Its planned proof combines the completed Theorem 1 with a separate Chudnovsky period theorem and an arithmetic lemma recovering the quasi-period of an integer combination. These additional dependencies remain to be formalized. The mission's completed main goal and nine paper-related milestones continue to record the original scope.

Selected references

• Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions, Proceedings of the Edinburgh Mathematical Society, published online 17 June 2026, pp. 1–33. DOI. Target: Theorem 1; supporting identities: §4, equations (5) and (6).
• NIST Digital Library of Mathematical Functions, Chapter 23, §23.2: Definitions and Periodic Properties, accessed 4 September 2026. Zeta normalization: equation 23.2.5; quasi-period convention: equation 23.2.11.
• Mathlib contributors, Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, pinned revision 0df444a360eaa60ab8c11dca51a86af692955474 (Lean 4.33.1).