Prove2Me

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

Algebra

92 missions · 41 completed

The study of algebraic structures — groups, rings, and fields — and, through algebraic geometry, the geometry of the solution sets of polynomial equations. Using commutative algebra to describe these varieties, the field provides a common language of symmetry and structure that underlies much of modern mathematics.

Missions

Group Theory·Captain: wurtle

The Kervaire theorem for groupsResearch Paper

Motivation

Given a group AA, adjoin one new generator tt and impose one relation w=1w=1, where ww is a word in tt and elements of AA. Can the result collapse to the trivial group when AA is nontrivial? The Kervaire conjecture says no. It arose from Kervaire's 1965 characterization of high-dimensional knot groups, which involves groups normally generated by a single element, and it is one of the best-known problems about equations over groups: when does an equation w(t)=1w(t)=1 with coefficients in AA have a solution in some group containing AA?

Timeline

  • 1962. Gerstenhaber and Rothaus prove that nonsingular systems of equations over finite groups are solvable in finite overgroups, using unitary groups and degree theory (doi:10.1073/pnas.48.9.1531); this gives the result for residually finite groups.
  • 1965. Kervaire characterizes high-dimensional knot groups (doi:10.24033/bsmf.1624); the group-theoretic Kervaire problem is traced to this setting.
  • 1983. Howie studies equations of length three over groups (doi:10.1017/S0013091500028108).
  • 1993. Klyachko proves unimodular injectivity for torsion-free groups (doi:10.1080/00927879308824692).
  • 2005. Klyachko records the reduction showing that universal nontriviality is equivalent to unimodular injectivity (doi:10.1007/s10469-005-0023-y).
  • 2008. Pestov records the extension to hyperlinear groups (doi:10.2178/bsl/1231081461).
  • 2012. Klyachko and Lurye prove injectivity for arbitrary coefficient groups after imposing wm=1w^m=1, m≥2m\ge2 (doi:10.1016/j.jpaa.2011.06.020).
  • 2017. Klyachko and Thom develop new topological methods for equations over groups (doi:10.2140/agt.2017.17.331).
  • 2024–2026. Kawauchi publishes a proposed resolution via ribbon sphere-links; Chen gives a new proof of the torsion-free case via the complexity of surfaces (arXiv:2302.09811).

The source of this mission, an OpenAI preprint dated September 24, 2026, proves unimodular coefficient injectivity for every group by a route through spectral phase and a fixed-space theorem for unitary matrices.

Setting

Let AA be a group, ⟨t⟩≅Z\langle t\rangle\cong\mathbb Z, and H=A∗⟨t⟩H=A*\langle t\rangle the free product. Let p:H→Zp:H\to\mathbb Z be the homomorphism that kills AA and sends tt to 11; p(w)p(w) is the exponent sum of tt in ww. A word w∈Hw\in H is unimodular if p(w)=±1p(w)=\pm1. Write ⟨ ⁣⟨w⟩ ⁣⟩H\langle\!\langle w\rangle\!\rangle_H for the normal closure of ww in HH. The coefficient map is the composite

A↪H↠H/⟨ ⁣⟨w⟩ ⁣⟩H.A\hookrightarrow H\twoheadrightarrow H/\langle\!\langle w\rangle\!\rangle_H.

Its injectivity is equivalent to solvability of w(t)=1w(t)=1 over AA: there is an overgroup B⊇AB\supseteq A and b∈Bb\in B with w(b)=1w(b)=1.

Formalization targets

Goal: Theorem 1.1

∀A, ∀w∈A∗⟨t⟩ with p(w)=±1:A⟶(A∗⟨t⟩)/⟨ ⁣⟨w⟩ ⁣⟩H is injective.\forall A,\ \forall w\in A*\langle t\rangle\ \text{with}\ p(w)=\pm1:\qquad A\longrightarrow (A*\langle t\rangle)/\langle\!\langle w\rangle\!\rangle_H\ \text{is injective}.

The Lean statement OAI.Kervaire.coefficient_injective is open on the platform.

Significance

Theorem 1.1 immediately gives the Kervaire conjecture (Corollary 1.2): if A≠1A\ne1 then (A∗⟨t⟩)/⟨ ⁣⟨w⟩ ⁣⟩≠1(A*\langle t\rangle)/\langle\!\langle w\rangle\!\rangle\ne1 for every ww, since for p(w)=d≠±1p(w)=d\ne\pm1 the quotient maps onto Z/dZ\mathbb Z/d\mathbb Z. It proves the unimodular case of the stronger Kervaire–Laudenbach conjecture with no hypothesis on AA: no torsion-freeness, residual finiteness, hyperlinearity or countability. The paper's companion work extends the method to nonsingular systems of equations (Howie's conjecture).

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The statement is short and entirely algebraic, which makes it an attractive formalization target; Mathlib already provides free products and normal closures.

Difficulty

The classical Gerstenhaber–Rothaus argument solves the equation in a unitary group and needs AA to embed in (an ultraproduct of) unitary groups, which is not known for arbitrary groups. Torsion in AA blocks the diagrammatic and topological arguments that work in the torsion-free case. A proof for every group therefore needs a representation available for all groups (the left regular representation, with its faithful finite trace) together with an argument that does not rely on finite-dimensional approximation of AA.

Formalization scope

  • The free product is Monoid.Coprod A (Multiplicative ℤ); the exponent sum is Multiplicative.toAdd (Monoid.Coprod.snd w).
  • Unimodular w is exponentSum w = 1 ∨ exponentSum w = -1.
  • The quotient is by Subgroup.normalClosure {w}, and coefficientMap w is the quotient map composed with Monoid.Coprod.inl.
  • No hypothesis is placed on AA; the group may live in any universe.

A complete development needs the group von Neumann algebra of AA (or at least its trace), the spectral phase of unitaries and its subadditivity, a degree computation on a compact manifold of unitaries with fixed kk-planes, and corner-labelled planar diagrams with Euler-characteristic estimates. Contributions formalizing Corollary 1.2 from Theorem 1.1, Lemma 2.1 (subadditivity of spectral phase) and Lemma 3.1 (fixed-space lemma) are welcome.

Selected references

2 thms1 active userReviewed
Group Theory·Captain: wurtle

The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjectureResearch Paper

Motivation

The Hattori–Stallings trace refines the rank of a finitely generated projective module over a group ring CG\mathbb CG into one complex number per conjugacy class of GG. These numbers enter group-ring Euler characteristics, where they retain information that an ordinary numerical Euler characteristic forgets. Bass's trace conjecture (complex group-ring form) predicts that the trace of every projective module vanishes at every conjugacy class of an element of infinite order. For torsion-free groups this forces the trace to be an integer rank, and that in turn implies the Kaplansky idempotent conjecture: a group ring kGkG of a torsion-free group over a field of characteristic zero has no idempotents other than 00 and 11. Both questions date from the 1960s–1970s and were previously known only for restricted classes of groups (linear, elementary amenable, amenable, hyperbolic, or groups satisfying the Farrell–Jones conjecture).

This mission asks for a formal proof of the complex Bass trace conjecture for all discrete groups, with the torsion-free consequences as a milestone, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

  • 1965 — Hattori (Nagoya Math. J. 1965) and Stallings (Topology 1965) introduce the rank element of a projective module.
  • 1973 — Formanek proves the characteristic-zero idempotent statement for torsion-free groups with the ascending chain condition on subgroups (Canad. J. Math. 1973).
  • 1976–1979 — Bass formulates the trace conjectures and proves complex trace vanishing for linear groups (Invent. Math. 1976; Homological Group Theory 1979).
  • 1983 — Linnell restricts the possible coefficients of the integral trace (Proc. LMS 1983).
  • 1985–1986 — Cyclic homology approaches: Connes (Publ. IHÉS 1985), Burghelea (Comment. Math. Helv. 1985), Eckmann (Comment. Math. Helv. 1986).
  • 1998 — Burger and Valette revisit Kaplansky's and Zalesskii's theorems: the canonical trace of an idempotent lies in [0,1][0,1] and is rational (J. Lie Theory 1998).
  • 2002 — Mineyev–Yu (Invent. Math. 2002) and Puschnigg (Invent. Math. 2002) treat torsion-free hyperbolic groups in Cr∗(G)C^*_r(G).
  • 2003–2008 — Elementary amenable groups (Farrell–Linnell, Math. Ann. 2003); amenable groups (Berrick–Chatterji–Mislin, Math. Ann. 2004); groups satisfying Farrell–Jones (Bartels–Lück–Reich, J. Topol. 2008).
  • September 2026 — The OpenAI preprint claims the complex Bass conjecture for every group (Theorem 1.1, p. 3) and the characteristic-zero idempotent conjecture (Corollary 1.2, p. 3).

Setting

Let GG be a group and CG\mathbb CG its complex group ring. K0(CG)K_0(\mathbb CG) is the Grothendieck group of finitely generated projective right CG\mathbb CG-modules. An idempotent matrix e∈Mq(CG)e\in M_q(\mathbb CG) represents the module e(CG)qe(\mathbb CG)^q; its Hattori–Stallings trace is the class of ∑ieii\sum_i e_{ii} in CG/[CG,CG]\mathbb CG/[\mathbb CG,\mathbb CG], extended additively to K0K_0. Identifying this quotient with finitely supported functions on conjugacy classes (sum the coefficients over each class), HSG(x)(C)\mathrm{HS}_G(x)(C) is the coefficient of x∈K0(CG)x\in K_0(\mathbb CG) at the class CC.

For the corollary: GG is torsion-free if its only element of finite order is 11. The canonical trace is τG(∑agg)=a1\tau_G(\sum a_gg)=a_1, the augmentation is ϵG(∑agg)=∑ag\epsilon_G(\sum a_gg)=\sum a_g, τG,q(b)=∑iτG(bii)\tau_{G,q}(b)=\sum_i\tau_G(b_{ii}), and ϵG,q\epsilon_{G,q} applies ϵG\epsilon_G entrywise. τG,∗:K0(CG)→C\tau_{G,*}:K_0(\mathbb CG)\to\mathbb C is the coefficient at [1][1], and rkϵ:K0(CG)→Z\mathrm{rk}_\epsilon:K_0(\mathbb CG)\to\mathbb Z is the augmentation rank.

Formalization targets

Milestone: Corollary 1.2 (p. 3)

Let GG be torsion-free. (i) For every q≥1q\ge1 and idempotent e∈Mq(CG)e\in M_q(\mathbb CG), τG,q(e)=rank⁡CϵG,q(e)\tau_{G,q}(e)=\operatorname{rank}_{\mathbb C}\epsilon_{G,q}(e); hence τG,∗=rkϵ\tau_{G,*}=\mathrm{rk}_\epsilon and τG,∗(K0(CG))=Z\tau_{G,*}(K_0(\mathbb CG))=\mathbb Z. (ii) For every commutative unital domain RR of characteristic zero, every e∈RGe\in RG with e2=ee^2=e is 00 or 11.

Goal: Theorem 1.1 (p. 3)

For every group GG, every x∈K0(CG)x\in K_0(\mathbb CG) and every g∈Gg\in G of infinite order,

HSG(x)([g])=0;\mathrm{HS}_G(x)([g])=0;

equivalently, HSG(x)\mathrm{HS}_G(x) is supported on conjugacy classes of finite-order elements.

Significance

The result itself. Theorem 1.1 holds for arbitrary groups, with no amenability, finiteness, assembly-map or homological-dimension hypothesis. Combined with Linnell's restriction it gives the integral Bass conjecture (Corollary 9.1, p. 29) and, via Berrick–Chatterji–Mislin, statements about homotopy idempotents on manifolds (Corollary 9.2, p. 29). Corollary 1.2 settles Kaplansky's idempotent conjecture in characteristic zero, including over commutative domains rather than only fields. The analytic Kadison–Kaplansky statement in Cr∗(G)C^*_r(G) and the positive-characteristic idempotent problem are not addressed.

Formalizing it. The statements need only group rings (MonoidAlgebra), matrices, projective modules and conjugacy classes, all in Mathlib, so both are precise algebraic targets. The proof combines finite path sums in the group with a Pfaffian cocycle (Sections 7–8) and a geometric vanishing theorem for sparse simplicial cycles built from separating filtrations, simplicial volume estimates and free actions on Cantor-type spaces (Sections 2–6). None of this exists in Mathlib; the sparse-chain vanishing theorem (Theorem 2.1, p. 6) is of independent interest. No machine-checked proof of either conjecture, even for special group classes, is known.

Difficulty

Previous proofs pass through analytic completions or assembly maps and therefore need hypotheses on the group (amenability, hyperbolicity, Farrell–Jones), or through cyclic homology and need finite homological dimension of the reduced centralizers. The preprint turns an idempotent and an infinite-order element gg into simplicial cycles of every even dimension 2m2m with connected supports in one graph of bounded degree, and a cocycle evaluating to 2−mHSG(x)([g])2^{-m}\mathrm{HS}_G(x)([g]) (Propositions 7.3 and 8.3, pp. 24–27). The difficulty is to show that invariant cocycles vanish on such sparse cycles in high dimension for an arbitrary acting group H=CG(g)/⟨g⟩H=C_G(g)/\langle g\rangle, with no bound on its homological dimension (Theorem 2.1, p. 6): naive filling arguments need either amenability or finite dimensionality.

Formalization scope

  • K0K_0 of right modules is built in Lean as a quotient of the free abelian group on objects with a finitely generated projective Module (MonoidAlgebra ℂ G)ᵐᵒᵖ structure, by isomorphism and direct-sum relations (ModuleK0); the Hattori–Stallings trace factors through a presentation of each module by an idempotent matrix. Its values are ConjClasses G →₀ ℂ.
  • The goal states both the vanishing at infinite-order classes and the support inclusion in finite-order classes.
  • The corollary uses an idempotent-matrix presentation of K0(CG)K_0(\mathbb CG) (BassTrace.K0.Group), matrixTrace (sum of identity coefficients of diagonal entries) and augmentedMatrix; part (ii) quantifies over every commutative domain R with CharZero R.
  • TorsionFree G is the usual condition (every finite-order element is 11).
  • Neither statement is vacuous: idempotent matrices and projective modules exist for every GG, and the conclusions are equalities of explicit traces.

Selected references

2 thms1 active userReviewed
Representation Theory·Captain: wurtle

A counterexample to Tachikawa's second conjectureResearch Paper

Motivation

Let AA be a finite-dimensional algebra over a field. A finite-dimensional module MM is self-orthogonal if Ext⁡Ai(M,M)=0\operatorname{Ext}^i_A(M,M)=0 for every i>0i>0. Tachikawa's second conjecture asserts that over a self-injective algebra every self-orthogonal module is projective. It belongs to the cluster of homological conjectures around quasi-Frobenius algebras and dominant dimension recorded in Tachikawa's 1973 monograph, alongside the Nakayama, generalized Nakayama and Auslander–Reiten conjectures. Since Ext⁡Ai(M,A)=0\operatorname{Ext}^i_A(M,A)=0 automatically when AA is self-injective, it is exactly the self-injective case of the Auslander–Reiten conjecture. Enomoto and Marczinzik showed that Tachikawa's second conjecture for two-fold trivial extensions implies the Auslander–Reiten conjecture, so the two were expected to stand or fall together.

This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims a counterexample over a symmetric algebra. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).

Background

  • 1975 — Auslander and Reiten formulate the conjecture in their work on the generalized Nakayama conjecture (Proc. AMS 1975).
  • 1993 — Auslander, Ding and Solberg prove it for complete local complete intersections (J. Algebra 1993).
  • 1994–1995 — Schulz constructs a nonprojective module without self-extensions over a ring outside the Artin-algebra setting (Arch. Math. 1994) and quantum-exterior-algebra modules with eventually vanishing self-extensions (J. Aust. Math. Soc. 1995).
  • 2004 — Huneke and Leuschke prove the conjecture for excellent Cohen–Macaulay normal domains containing Q\mathbb Q (J. Algebra 2004); Huneke, Şega and Vraciu treat commutative Artinian local rings with radical cube zero (Illinois J. Math. 2004).
  • 2008 — Luo and Huang record the Gorenstein-projective variant (J. Algebra 2008).
  • 2010 — Christensen and Holm show that rings satisfying Auslander's condition satisfy the conjecture (Math. Z. 2010).
  • 2017–2022 — Erdmann's analysis of weakly symmetric algebras with J3=0J^3=0 (J. Aust. Math. Soc. 2017); Ringel and Zhang on short local algebras (J. LMS 2022).
  • 2026 — Zhang and Zhou prove the conjecture for split algebras with radical cube zero (arXiv:2609.08679) and for Igusa–Todorov algebras (arXiv:2609.14453); Xia for quantum complete intersections (arXiv:2609.24007); Enomoto shows that Tachikawa's second conjecture for two-fold trivial extensions implies the Auslander–Reiten conjecture (arXiv:2609.19172).
  • September 2026 — Two OpenAI preprints claim counterexamples: an explicit eight-simple Gorenstein-projective example (source) and a symmetric-algebra counterexample to Tachikawa's second conjecture (source).

Setting

Let k=F2(q,H1,H2)k=\mathbb F_2(q,H_1,H_2) be the rational function field in three algebraically independent variables. Write D=Hom⁡k(−,k)D=\operatorname{Hom}_k(-,k). A finite-dimensional kk-algebra AA is symmetric if A≅DAA\cong DA as AA-bimodules, where (a⋅f⋅b)(c)=f(bca)(a\cdot f\cdot b)(c)=f(bca); equivalently there is a kk-linear isomorphism e:A→DAe:A\to DA with e(ab)(c)=e(b)(ca)=e(a)(bc)e(ab)(c)=e(b)(ca)=e(a)(bc). Symmetric algebras are self-injective. For a finite-dimensional left AA-module MM, Ext⁡Ai(M,M)\operatorname{Ext}^i_A(M,M) is computed in the category of left AA-modules.

Formalization targets

Goal: Theorem 1.1 (p. 1)

There exist a finite-dimensional associative unital symmetric kk-algebra AA and a finite-dimensional unital left AA-module MM such that MM is not projective and

Ext⁡Ai(M,M)=0for every integer i>0.\operatorname{Ext}^i_A(M,M)=0\qquad\text{for every integer }i>0.

In particular Tachikawa's second conjecture is false, and since AA is self-injective the same pair is a symmetric counterexample to the Auslander–Reiten conjecture.

Significance

The result itself. The theorem disproves Tachikawa's second conjecture in the strongest natural class (symmetric algebras). Through an associated endomorphism algebra, the preprint further claims counterexamples to the classical, generalized and strong Nakayama conjectures, the Auslander–Gorenstein conjecture and the Wakamatsu tilting conjecture, persisting under every field extension (Corollary 1.2, p. 4), together with consequences for finitistic dimensions (Corollary 1.3, p. 5). Those corollaries are not part of this mission's goal. A companion preprint gives an explicit eight-simple triangular counterexample to the Auslander–Reiten conjecture.

Formalizing it. The statement uses only notions already in Mathlib (finite-dimensional algebras, projective modules, Abelian.Ext in ModuleCat), so it is a clean target. The proof needs trivial extensions Λ⋉DΛ\Lambda\ltimes D\Lambda, totally acyclic complexes, stable categories of symmetric algebras, Koszul computations of Ext⁡\operatorname{Ext}-algebras, and Hochschild bar complexes; these are reusable throughout representation theory.

Difficulty

Known non-examples come close but fail: Schulz's quantum exterior modules have vanishing higher self-extensions but nonzero Ext⁡1\operatorname{Ext}^1; Böhmler and Marczinzik have a commutative self-injective example with only Ext⁡1=Ext⁡2=0\operatorname{Ext}^1=\operatorname{Ext}^2=0. Vanishing in every positive degree requires controlling an infinite resolution. In the preprint, the passage to a symmetric algebra also requires vanishing of the negative part of a complete self-extension complex (condition (1.1), p. 2), which is what the transfer through the trivial extension A=Λ⋉DΛA=\Lambda\ltimes D\Lambda, M=A⊗ΛZM=A\otimes_\Lambda Z (Proposition 3.2, p. 12) consumes. Producing it needs two twists H1,H2H_1,H_2 acting by distinct scalars on every nonzero homogeneous self-map space, and genuine bimodule lifts of stable maps (Proposition 6.1, p. 21).

Formalization scope

  • The field is FractionRing (MvPolynomial (Fin 3) (ZMod 2)), i.e. F2(q,H1,H2)\mathbb F_2(q,H_1,H_2) with independent variables.
  • SymmetricOver k A asks for a kk-linear equivalence e : A ≃ₗ[k] Module.Dual k A with e (a*b) c = e b (c*a) and e (a*b) c = e a (b*c), i.e. a bimodule isomorphism A≅DAA\cong DA.
  • Counterexample asserts existence of A : Type with Ring and Algebra k structures, Module.Finite k A, symmetric; and M with compatible Module A, Module k (IsScalarTower), Module.Finite k M, ¬ Module.Projective A M, and Subsingleton (Abelian.Ext (ModuleCat.of A M) (ModuleCat.of A M) n) for all n > 0.
  • The nonprojectivity clause rules out M=0M=0 and semisimple AA, so the statement is not trivially satisfiable.

Selected references

2 thms1 active userReviewed
Representation Theory·Captain: wurtle

An explicit counterexample to the Auslander-Reiten conjectureResearch Paper

Motivation

In the representation theory of finite-dimensional algebras, vanishing of Ext⁡\operatorname{Ext} groups is the standard way of detecting projectivity homologically. The Auslander–Reiten conjecture (1975) asserts that a finitely generated module MM over an Artin algebra RR is projective as soon as

Ext⁡Ri(M,M⊕R)=0for every i>0.\operatorname{Ext}^i_R(M,M\oplus R)=0\qquad\text{for every }i>0.

It arose from Auslander and Reiten's work on the generalized Nakayama conjecture and sits in a web of homological conjectures (Nakayama, Tachikawa, Gorenstein-projective, Auslander–Gorenstein) that were long expected to hold. A module is Gorenstein-projective if it is a cokernel in a doubly infinite exact complex of finitely generated projectives that stays exact under Hom⁡R(−,R)\operatorname{Hom}_R(-,R); the Gorenstein-projective conjecture is the restriction of the Auslander–Reiten conjecture to such modules.

This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims an explicit counterexample to both conjectures. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).

Background

  • 1975 — Auslander and Reiten formulate the conjecture in their work on the generalized Nakayama conjecture (Proc. AMS 1975).
  • 1993 — Auslander, Ding and Solberg prove it for complete local complete intersections (J. Algebra 1993).
  • 1994–1995 — Schulz constructs a nonprojective module without self-extensions over a ring outside the Artin-algebra setting (Arch. Math. 1994) and quantum-exterior-algebra modules with eventually vanishing self-extensions (J. Aust. Math. Soc. 1995).
  • 2004 — Huneke and Leuschke prove the conjecture for excellent Cohen–Macaulay normal domains containing Q\mathbb Q (J. Algebra 2004); Huneke, Şega and Vraciu treat commutative Artinian local rings with radical cube zero (Illinois J. Math. 2004).
  • 2008 — Luo and Huang record the Gorenstein-projective variant (J. Algebra 2008).
  • 2010 — Christensen and Holm show that rings satisfying Auslander's condition satisfy the conjecture (Math. Z. 2010).
  • 2017–2022 — Erdmann's analysis of weakly symmetric algebras with J3=0J^3=0 (J. Aust. Math. Soc. 2017); Ringel and Zhang on short local algebras (J. LMS 2022).
  • 2026 — Zhang and Zhou prove the conjecture for split algebras with radical cube zero (arXiv:2609.08679) and for Igusa–Todorov algebras (arXiv:2609.14453); Xia for quantum complete intersections (arXiv:2609.24007); Enomoto shows that Tachikawa's second conjecture for two-fold trivial extensions implies the Auslander–Reiten conjecture (arXiv:2609.19172).
  • September 2026 — Two OpenAI preprints claim counterexamples: an explicit eight-simple Gorenstein-projective example (source) and a symmetric-algebra counterexample to Tachikawa's second conjecture (source).

Setting

Let k=F2(q,H1,H2)k=\mathbb F_2(q,H_1,H_2) be the field of rational functions in three algebraically independent variables over F2\mathbb F_2. A finite-dimensional kk-algebra Λ\Lambda is an Artin algebra. For a left Λ\Lambda-module ZZ, Ext⁡Λi(Z,−)\operatorname{Ext}^i_\Lambda(Z,-) is computed in the abelian category of left Λ\Lambda-modules. rad⁡Λ\operatorname{rad}\Lambda denotes the Jacobson radical. ZZ is Gorenstein-projective when Z≅coker⁡(P1→P0)Z\cong\operatorname{coker}(P_1\to P_0) for an exact complex (Pi)i∈Z(P_i)_{i\in\mathbb Z} of finitely generated projective modules such that every map Pi→QP_i\to Q into a projective QQ that vanishes on the image of Pi+1P_{i+1} factors through Pi→Pi−1P_i\to P_{i-1}. For a field extension K/kK/k, write ΛK=K⊗kΛ\Lambda_K=K\otimes_k\Lambda and ZK=K⊗kZZ_K=K\otimes_kZ.

Formalization targets

Goal: Theorem 1.1 (p. 2)

There exist a finite-dimensional kk-algebra Λ\Lambda and a finite-dimensional nonprojective left Λ\Lambda-module ZZ such that

Ext⁡Λi(Z,Z)=0=Ext⁡Λi(Z,Λ)(i≥1),\operatorname{Ext}^i_\Lambda(Z,Z)=0=\operatorname{Ext}^i_\Lambda(Z,\Lambda)\qquad(i\ge1),

ZZ is Gorenstein-projective, Λ/rad⁡Λ≅k8\Lambda/\operatorname{rad}\Lambda\cong k^8 as kk-algebras, and (rad⁡Λ)4≠0(\operatorname{rad}\Lambda)^4\ne0. All of these conclusions hold again for ΛK\Lambda_K and ZKZ_K for every field extension K/kK/k.

Significance

The result itself. The theorem refutes the Auslander–Reiten conjecture for Artin algebras and the Gorenstein-projective conjecture; by extending scalars to an algebraic closure it also refutes them over an algebraically closed field of characteristic two. Since Z⊕ΛZ\oplus\Lambda is then a nonprojective generator with no positive self-extensions, the generator formulation fails too. The structural data (88 simple modules, split, rad⁡4≠0\operatorname{rad}^4\ne0) place the example just outside the radical-cube-zero class where the conjecture is now known. The commutative case is not resolved.

Formalizing it. A formal proof would require Ext in module categories (available in Mathlib via Abelian.Ext), complete resolutions, triangular matrix algebras, trivial extensions and Hochschild cocycles, and base change of Ext under field extension. The counterexample is concrete, so much of the verification reduces to finite linear algebra over kk plus an infinite periodic-type resolution with uniform kernel formulas.

Difficulty

All positive results exploit some finiteness or rigidity (complete intersections, Cohen–Macaulay domains, radical cube zero, Auslander's condition), and the natural candidates for counterexamples (Schulz's quantum exterior algebra modules) have self-extensions that only vanish eventually, with Ext⁡1≠0\operatorname{Ext}^1\ne0. Vanishing in every positive degree, simultaneously against ZZ and Λ\Lambda, is the hard requirement. The preprint (Section 1.2, pp. 3–4) converts a suitable stable map over a symmetric algebra into a module over a triangular algebra Λ=(A0FA)\Lambda=\begin{pmatrix}A&0\\F&A\end{pmatrix} (Proposition 3.1, p. 6), uses powers of qq for a resolution with uniform kernels, and kills every positive self-extension with two independent twists H1,H2H_1,H_2, using that H1/H2H_1/H_2 has infinite multiplicative order.

Formalization scope

  • The field is FractionRing (MvPolynomial (Fin 3) (ZMod 2)), and the goal also asserts that the three generators are algebraically independent over F2\mathbb F_2.
  • The algebra and module are packaged as a System (types in Type, with Ring, Algebra K, Module, and IsScalarTower K Λ Z instances). Conclusions asserts finite dimensionality over kk, ¬ Module.Projective Λ Z, the totally acyclic witness, Subsingleton of Abelian.Ext in ModuleCat for all i>0i>0 against ZZ and against Λ\Lambda, a kk-algebra isomorphism Λ/Jac⁡(Λ)≅k8\Lambda/\operatorname{Jac}(\Lambda)\cong k^8, and Jac⁡(Λ)4≠⊥\operatorname{Jac}(\Lambda)^4\ne\bot.
  • Field extension is quantified over every field E with Algebra K E in an arbitrary universe; the module structure on E⊗kZE\otimes_k Z must satisfy (a⊗r)(b⊗z)=ab⊗rz(a\otimes r)(b\otimes z)=ab\otimes rz, which pins it to the standard one.
  • The totally acyclic condition tests exactness of Hom⁡(−,Q)\operatorname{Hom}(-,Q) for all projective QQ, which for complexes of finitely generated projectives is equivalent to the source's Hom⁡(−,Λ)\operatorname{Hom}(-,\Lambda) condition.
  • No trivialization: nonprojectivity and rad⁡4≠0\operatorname{rad}^4\ne0 exclude the zero and semisimple cases.

Selected references

2 thms1 active userReviewed
Category TheoryRepresentation Theory·Captain: wurtle

An algebra of infinite little finitistic dimensionResearch Paper

Motivation

Every module over a ring has a projective resolution, and its length, the projective dimension, measures how far the module is from being projective. Over a finite-dimensional algebra, some modules have infinite projective dimension; the finitistic dimension conjectures ask whether, among the modules whose projective dimension is finite, these finite values are bounded. The questions were publicized by Bass in 1960 and became central problems in the representation theory of finite-dimensional algebras, tied to many other homological conjectures (Nakayama, Gorenstein symmetry, Auslander–Reiten), each of which would follow from finiteness of the finitistic dimension.

Timeline

  • 1960. Bass publicizes the finitistic-dimension questions (doi:10.1090/S0002-9947-1960-0157984-8).
  • 1991. Green, Kirkman and Kuzmanovich prove little finitistic finiteness for finite-dimensional monomial algebras (doi:10.1016/0021-8693(91)90062-D); Green and Huisgen-Zimmermann treat Artin algebras with radical cube zero.
  • 1992. Huisgen-Zimmermann constructs monomial algebras whose little and big finitistic dimensions differ (nn versus n+1n+1), so the two invariants are not equal in general (doi:10.1007/BF02100610).
  • 1995. Huisgen-Zimmermann's survey "a tale of 3.5 decades" describes the state of the problems (doi:10.1007/978-94-011-0443-2_41).
  • 2005. Igusa and Todorov introduce syzygy invariants and prove finiteness for Artin algebras of representation dimension at most three.
  • 2019. Rickard shows that if injective modules generate the unbounded derived category, then the big finitistic dimension is finite (doi:10.1016/j.aim.2019.106735).
  • 2024. Cummings proves that universal little finitistic finiteness is equivalent to its left–right symmetry (doi:10.1112/blms.12954).

The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample to the little finitistic-dimension conjecture over C\mathbb C. A companion OpenAI preprint independently gives a characteristic-two example.

Setting

Let AA be a finite-dimensional unital algebra over C\mathbb C. For a left AA-module NN, pd⁡AN∈{0,1,2,… }∪{∞}\operatorname{pd}_AN\in\{0,1,2,\dots\}\cup\{\infty\} is the minimal length of a projective resolution. The little finitistic dimension is

findim⁡A=sup⁡{pd⁡AN: N finitely generated left A-module, pd⁡AN<∞},\operatorname{findim}A=\sup\{\operatorname{pd}_AN:\ N\ \text{finitely generated left } A\text{-module},\ \operatorname{pd}_AN<\infty\},

and the big finitistic dimension Findim⁡A\operatorname{Findim}A is the same supremum over all left modules. Over a finite-dimensional algebra, finitely generated and finite-dimensional modules coincide. The little finitistic-dimension conjecture asserts findim⁡A<∞\operatorname{findim}A<\infty for every such AA.

Injective left modules generate if the smallest triangulated subcategory of the unbounded derived category of left modules that contains them and is closed under arbitrary coproducts is the whole category.

Formalization targets

Goal: Theorem 1.1

∃ A finite-dimensional over C:∀m≥1 ∃Nm finitely generated with 2m−2≤pd⁡ANm<∞; hence findim⁡A=∞.\exists\ A\ \text{finite-dimensional over } \mathbb C:\quad \forall m\ge1\ \exists N_m\ \text{finitely generated with}\ 2m-2\le\operatorname{pd}_AN_m<\infty;\ \text{hence}\ \operatorname{findim}A=\infty.

The Lean statement OAI.LittleFinitistic.Main.exists_counterexample is open on the platform.

Milestone: Corollary 1.2

∃ Λ: findim⁡Λ=Findim⁡Λ=∞,findim⁡Λop=Findim⁡Λop=0,\exists\ \Lambda:\ \operatorname{findim}\Lambda=\operatorname{Findim}\Lambda=\infty,\quad \operatorname{findim}\Lambda^{\rm op}=\operatorname{Findim}\Lambda^{\rm op}=0,

injective left Λ\Lambda-modules do not generate, and injective right Λ\Lambda-modules do.

Significance

Theorem 1.1 refutes the little finitistic-dimension conjecture: a single finite-dimensional algebra has finitely generated modules with terminating projective resolutions of unbounded length. Since findim⁡≤Findim⁡\operatorname{findim}\le\operatorname{Findim}, it also refutes the big version for Artin algebras, and by Rickard's theorem gives an algebra for which injectives do not generate the derived category. Corollary 1.2 shows that finiteness can fail on one side and hold on the other in the most extreme way, in contrast with Cummings' equivalence of universal finiteness and left–right symmetry.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Because many homological conjectures were known to follow from the finitistic-dimension conjecture, an independent check of a counterexample is of direct interest.

Difficulty

Positive results cover large classes (monomial, radical cube zero, representation dimension at most three), so a counterexample must escape all of them. The finitistic dimension of one fixed algebra must be unbounded, which requires encoding an unbounded family of terminating processes into fixed finite data. The paper realizes a "selection process" from an infinite finitely presented group algebra by a single bounded bimodule complex over a finite-dimensional algebra; making this realization uniform in the input module, and turning it into ordinary projective resolutions over a trivial extension, are the main obstacles.

Formalization scope

  • Algebras are A : Type with [Ring A] [Algebra ℂ A] and FiniteDimensional ℂ A; modules are objects of ModuleCat.{0} A, finiteness is Module.Finite A N.
  • projectiveDimension is Mathlib's CategoryTheory.projectiveDimension, valued in WithBot ℕ∞, equal to ⊤ for infinite dimension; littleFinitisticDimension and bigFinitisticDimension are suprema over modules of finite projective dimension.
  • Right modules are left modules over Aᵐᵒᵖ.
  • InjectivesGenerate uses HasDerivedCategory.standard and quantifies over isomorphism-closed triangulated properties closed under coproducts indexed by Type u and containing all injectives in degree 0.

A complete development needs derived tensor products of bimodule complexes, trivial extension algebras D⋉XD\ltimes X and their bar resolutions, finite presentations of group algebras and their finite-dimensional representations, and (for the milestone) Rickard's theorem and Cummings' triangular algebra. Contributions formalizing Proposition 2.1 (selection), Theorem 4.1 (tensor realization) and Proposition 6.1 (bar splitting) are welcome.

Selected references

2 thms1 active userReviewed
CombinatoricsNumber Theory·Captain: wurtle

The circulant Hadamard conjectureResearch Paper

Motivation

A Hadamard matrix of order nn is an n×nn\times n matrix with entries ±1\pm1 whose rows are mutually orthogonal, HHT=nInHH^{\mathsf T}=nI_n. Such matrices are extremal for Hadamard's determinant bound and are used throughout coding theory, experimental design and signal processing. Imposing a circulant structure, where every row is a cyclic shift of the first, links the problem to cyclic difference sets and to binary sequences with ideal periodic autocorrelation. The order-4 example with first row (−1,1,1,1)(-1,1,1,1) is easy to find; the circulant Hadamard conjecture, traditionally attributed to Ryser (1963), asserts that apart from the trivial order 1 there are no others.

The question is closely tied to Barker sequences, binary sequences with the smallest possible aperiodic autocorrelations, which are used as radar pulse-compression codes. Only lengths 2,3,4,5,7,11,132,3,4,5,7,11,13 are known, and the long-standing Barker-sequence conjecture says there are no others.

Timeline

Several complete proofs have been claimed (Oh-Hashi 2016, Orozco López 2019, Morris 2023, Gallardo 2024, Manjhi–Kumar 2025). The source of this mission is an OpenAI preprint dated September 23, 2026, which proves the conjecture by an argument with cyclotomic character values over the group ring Z[i][Cu2]\mathbb Z[i][C_{u^2}].

Setting

A real n×nn\times n matrix HH is circulant if there is a function h:Z/nZ→Rh:\mathbb Z/n\mathbb Z\to\mathbb R with Hij=h(j−i)H_{ij}=h(j-i), indices taken modulo nn. It is a sign Hadamard matrix if every entry is 11 or −1-1 and

HHT=n In.HH^{\mathsf T}=n\,I_n.

For a circulant sign matrix with first row hh, the periodic autocorrelations are Ph(t)=∑jhjhj+tP_h(t)=\sum_{j}h_jh_{j+t}; the Hadamard condition says Ph(t)=0P_h(t)=0 for 1≤t<n1\le t<n.

A Barker sequence of length nn is a∈{−1,1}na\in\{-1,1\}^n with aperiodic autocorrelations

Ca(t)=∑j=0n−t−1ajaj+t,∣Ca(t)∣≤1(1≤t<n).C_a(t)=\sum_{j=0}^{n-t-1}a_ja_{j+t},\qquad |C_a(t)|\le1\quad(1\le t<n).

Formalization targets

Goal: Theorem 1.1

For n≥1:∃ a real circulant Hadamard matrix of order n  ⟺  n∈{1,4}.\text{For } n\ge1:\quad \exists\ \text{a real circulant Hadamard matrix of order } n\iff n\in\{1,4\}.

The Lean statement OAI.CirculantHadamard.exists_iff_order_one_or_four is open on the platform.

Milestone: Corollary 1.2, even case

a∈{−1,1}n Barker, n≥1 even ⟹ n∈{2,4}.a\in\{-1,1\}^n\ \text{Barker},\ n\ge1\ \text{even}\ \Longrightarrow\ n\in\{2,4\}.

Combined with the classical odd-length classification, this gives the Barker length list {2,3,4,5,7,11,13}\{2,3,4,5,7,11,13\}.

Significance

Theorem 1.1 closes a problem open since the early 1960s and, through the even-length reduction, completes the classification of Barker-sequence lengths. Equivalently, it shows that cyclic difference sets with parameters (4u2, 2u2−u, u2−u)(4u^2,\,2u^2-u,\,u^2-u) exist only for u=1u=1. It also explains, in a single statement, the computational evidence of Logan and Mossinghoff and the arithmetic restrictions of Turyn and of Leung–Schmidt.

The result is proved in an OpenAI preprint that has not been peer reviewed; given the number of earlier claimed proofs, an independent machine-checked proof would be especially valuable. No formal proof of either statement exists; the formalization would also produce reusable group-ring and cyclotomic machinery.

Difficulty

The orthogonality condition is a norm equation hh∗=nhh^*=n in the group ring Z[Cn]\mathbb Z[C_n], and every character sends hh to a cyclotomic integer of absolute value n\sqrt n. Classical arguments use such character values one at a time, through factorization of ideals in cyclotomic fields, and stop at the case n=4u2n=4u^2 with uu odd and divisible by several primes. The obstruction must combine information from all prime divisors of uu simultaneously and use the fact that the coefficients are signs, not arbitrary integers; norm equations alone do have solutions at these orders.

Formalization scope

  • RealMatrix n := Matrix (Fin n) (Fin n) ℝ; IsCirculant H asks for h : Fin n → ℝ with H i j = h (j - i), where subtraction in Fin n is modular.
  • IsSignHadamard H is entrywise IsSign (equal to 11 or −1-1) together with H * H.transpose = (n : ℝ) • 1.
  • The goal assumes 0 < n, matching the paper's "positive integer nn".
  • The Barker milestone uses integer sequences Fin n → ℤ with IsSign entries and aperiodic h k = Σ_{j<n-k} h_j h_{j+k}, bounded by 11 in absolute value for 0<k<n0<k<n.

A complete development needs group rings of finite cyclic groups, characters and cyclotomic integers, localization at primes above pp, and Kronecker's theorem that an algebraic integer all of whose conjugates have absolute value one is a root of unity. Contributions formalizing Proposition 2.2 (the order restriction n=4u2n=4u^2, uu odd), Lemma 3.1 (character comparison) and Proposition 3.4 (alternating character products are roots of unity of odd order) are welcome.

Selected references

2 thms1 active userReviewed
CombinatoricsRepresentation Theory·Captain: wurtle

Combinatorial invariance of Kazhdan–Lusztig polynomialsResearch Paper

Motivation

Kazhdan–Lusztig polynomials Pu,b(q)P_{u,b}(q) are integer polynomials attached to pairs u≤bu\le b of elements of a Coxeter group. They were introduced through the canonical basis of the Hecke algebra (Kazhdan–Lusztig, 1979). For Weyl groups they compute local intersection cohomology of Schubert varieties, and they enter the Kazhdan–Lusztig conjectures on characters of highest-weight representations. Their definition uses the simple generators of the group, yet in every known example Pu,bP_{u,b} seemed to depend only on the Bruhat interval [u,b][u,b] as an abstract partially ordered set. The combinatorial invariance conjecture, attributed to Lusztig and Dyer, asserts this: if two Bruhat intervals, possibly in different Coxeter groups, are isomorphic as posets, their Kazhdan–Lusztig polynomials coincide.

This mission asks for a formal proof of the conjecture, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

  • 1979–1980 — Kazhdan and Lusztig define the polynomials (Invent. Math. 1979) and interpret them via Schubert varieties (Proc. Sympos. Pure Math. 36, 1980).
  • 1987–1993 — Dyer's thesis and papers on reflection subgroups and the Bruhat graph (J. Algebra 1990; Compositio 1991); the conjecture's published formulation for finite Coxeter systems and the reconstruction of the Bruhat graph from the interval order.
  • 2000–2006 — Lower intervals [1,b][1,b]: du Cloux (Adv. Math. 2003), Brenti for symmetric groups (EJC 2004), and for all Coxeter systems Brenti–Caselli–Marietti (Adv. Math. 2006) and Delanoy (J. Alg. Combin. 2006).
  • 2001–2014 — Moment-graph and Soergel-bimodule machinery: Braden–MacPherson (Math. Ann. 2001), Fiebig (Trans. AMS 2008), Soergel (J. Inst. Math. Jussieu 2007), Elias–Williamson (Annals 2014).
  • 2007–2021 — Short intervals (Incitti, JCTA 2007); the coefficient of qq in simply-laced type (Patimo, IMRN 2021).
  • 2022–2026 — Hypercube decompositions guided by machine learning (Blundell–Buesing–Davies–Veličković–Williamson, Represent. Theory 2022); Barkley–Gaetz (Math. Ann. 2025; IMRN 2026); Barkley–Gaetz–Lam: invariance of the qq-coefficient in general and full invariance up to rank six (arXiv:2601.07793); Esposito–Marietti–Stella up to rank ten in finite Weyl groups (arXiv:2509.16433).
  • September 2026 — The OpenAI preprint claims the full conjecture for arbitrary Coxeter systems (Theorem 1.1, p. 2).

Setting

A Coxeter system (W,S)(W,S) is a group WW with a generating set SS of involutions subject only to relations (st)mst=1(st)^{m_{st}}=1. Write ℓ\ell for word length in SS. A reflection is a conjugate of an element of SS. Bruhat order is the partial order generated by x<txx<tx whenever tt is a reflection and ℓ(tx)>ℓ(x)\ell(tx)>\ell(x); the interval [u,b]={x:u≤x≤b}[u,b]=\{x:u\le x\le b\} is finite and graded of rank ℓ(b)−ℓ(u)\ell(b)-\ell(u), even when WW is infinite. The equal-parameter R-polynomials Rx,yR_{x,y} and Kazhdan–Lusztig polynomials Px,yP_{x,y} are the unique families with Rx,x=Px,x=1R_{x,x}=P_{x,x}=1, Rx,y=Px,y=0R_{x,y}=P_{x,y}=0 unless x≤yx\le y, the recursion: for s∈Ss\in S with sy<ysy<y,

Rx,y={Rsx,sy,sx<x,(q−1)Rx,sy+q Rsx,sy,sx>x,R_{x,y}=\begin{cases}R_{sx,sy}, & sx<x,\\ (q-1)R_{x,sy}+q\,R_{sx,sy}, & sx>x,\end{cases}

the degree bound deg⁡Px,y<(ℓ(y)−ℓ(x))/2\deg P_{x,y}<(\ell(y)-\ell(x))/2 for x<yx<y, and the inversion formula

qℓ(y)−ℓ(x)Px,y(q−1)=∑x≤z≤yRx,z(q) Pz,y(q).q^{\ell(y)-\ell(x)}P_{x,y}(q^{-1})=\sum_{x\le z\le y}R_{x,z}(q)\,P_{z,y}(q).

Formalization targets

Goal: Theorem 1.1 (p. 2)

Let (W,S)(W,S) and (W′,S′)(W',S') be arbitrary Coxeter systems, u≤bu\le b in WW and u′≤b′u'\le b' in W′W'. If ι:[u,b]→[u′,b′]\iota:[u,b]\to[u',b'] is an isomorphism of posets (a bijection preserving and reflecting order), then

Pu,bW(q)=Pu′,b′W′(q).P^{W}_{u,b}(q)=P^{W'}_{u',b'}(q).

The isomorphism carries no labels or root data; the groups may be infinite and noncrystallographic.

Significance

The result itself. It shows that a Kazhdan–Lusztig polynomial, defined algebraically from the Hecke algebra, is determined by a finite poset. Restricting ι\iota to subintervals gives the same for every Px,yP_{x,y} with u≤x≤y≤bu\le x\le y\le b, and hence for the R-polynomials (Corollary 6.1, p. 29). For Weyl groups this means that local intersection cohomology of Schubert varieties is determined by the Bruhat poset. It settles a question open since the 1980s that had been verified only for lower intervals, short intervals, low ranks, and single coefficients.

Formalizing it. Mathlib has Coxeter systems and their length function but no Bruhat order, Hecke algebra, or Kazhdan–Lusztig theory. The proof uses reflection orders (Dyer's path formula, Theorem 2.2, p. 7), Braden–MacPherson moment-graph sheaves over a reflection-faithful real realization (Theorem 2.3, p. 8), and the Elias–Williamson character theorem as external inputs. Building these would be a substantial, reusable contribution to formal representation theory.

Difficulty

The defining recursion uses a simple generator ss with sy<ysy<y, but a poset isomorphism need not carry simple generators or reflections to anything recognisable, and need not respect root labels. Dyer's reconstruction recovers all reflection edges of the Bruhat graph from the order (Theorem 3.4, p. 12) but not their labels. Lanini's moment-graph invariance requires compatible label automorphisms, which an abstract isomorphism does not provide. The preprint therefore keeps the two realizations separate, transports reflection orders through maximal dihedral subintervals (Proposition 3.5, p. 13), counts later edges exactly, and compares images of edges in two different sheaves by a reciprocal inequality that is then forced to be an equality (Sections 5–6).

Formalization scope

  • Coxeter systems are Mathlib CoxeterSystem M W for arbitrary index types and groups; the two systems may live in different universes.
  • BruhatLE is the reflexive–transitive closure of x→txx\to tx with tt a reflection and ℓ(x)<ℓ(tx)\ell(x)<\ell(tx), i.e. strong Bruhat order (not weak order). Interval cs u b carries this order; ι is an order isomorphism ≃o.
  • klPolynomial is the second component of Classical.epsilon (NormalizedKL cs), where NormalizedKL encodes exactly the normalization above (R-recursion with left multiplication, diagonal and vanishing conditions, 2deg⁡P<ℓ(y)−ℓ(x)2\deg P<\ell(y)-\ell(x), and the inversion formula with Polynomial.reflect). Existence and uniqueness of such families is the classical Kazhdan–Lusztig theorem, and a proof of the goal has to establish them, since otherwise Classical.epsilon returns an arbitrary pair.
  • Sums over intervals use finsum; intervals are finite, so this is the ordinary sum.
  • The hypotheses u≤bu\le b, u′≤b′u'\le b' are explicit; there is no vacuous reading.

Welcome contributions: Bruhat order and its basic properties (subword property, finiteness of intervals), R-polynomials, and existence and uniqueness of Kazhdan–Lusztig polynomials for arbitrary Coxeter systems.

Selected references

2 thms1 active userReviewed
Complexity TheoryTheoretical Computer Science·Captain: wurtle

Homogeneous depth-five lower bounds for iterated matrix multiplicationResearch Paper

Motivation

Iterated matrix multiplication asks for the (1,1)(1,1) entry of a product of dd matrices of size w×ww\times w with independent variable entries,

IMMw,d=(X(1)⋯X(d))1,1=∑i1,…,id−1∈[w]x1,i1(1)xi1,i2(2)⋯xid−1,1(d).\mathrm{IMM}_{w,d}=\bigl(X^{(1)}\cdots X^{(d)}\bigr)_{1,1}=\sum_{i_1,\dots,i_{d-1}\in[w]}x^{(1)}_{1,i_1}x^{(2)}_{i_1,i_2}\cdots x^{(d)}_{i_{d-1},1}.

It has polynomial-size arithmetic circuits when depth is unrestricted and is complete for algebraic branching programs, so it is the standard test case for the cost of restricting circuit depth. Depth-reduction theorems (Agrawal–Vinay, Koiran, Tavenas) show that any polynomial-size circuit for a degree-dd polynomial can be flattened to homogeneous depth four with size NO(d)N^{O(\sqrt d)}; lower bounds of the form NΩ(d)N^{\Omega(\sqrt d)} at small depth are therefore exactly at the threshold that depth reduction permits, and improving them slightly would separate general circuits from formulas. Nisan and Wigderson asked for an explicit homogeneous polynomial requiring superpolynomial size at constant depth, even at depth five.

Timeline

  • 1995. Nisan and Wigderson introduce partial-derivative measures and ask for superpolynomial homogeneous constant-depth lower bounds, even at depth five.
  • 2008–2015. Agrawal–Vinay, Koiran (doi:10.1016/j.tcs.2012.03.041) and Tavenas (doi:10.1016/j.ic.2014.09.004) reduce general circuits to homogeneous depth four of size NO(d)N^{O(\sqrt d)}.
  • 2014. Gupta, Kamath, Kayal and Saptharishi develop shifted partial derivatives (doi:10.1145/2629541); Kayal, Limaye, Saha and Srinivasan prove exponential bounds for homogeneous depth-four formulas.
  • 2015. Fournier, Limaye, Malod and Srinivasan prove IMM lower bounds for restricted depth-four formulas (doi:10.1137/140990280); Bera and Chakrabarti prove a depth-five IMM lower bound with bounded bottom support (doi:10.4230/LIPIcs.CCC.2015.183).
  • 2017. Kumar and Saraf prove dΩ(d)d^{\Omega(\sqrt d)} for homogeneous depth-four circuits computing IMMd5,d\mathrm{IMM}_{d^5,d} (doi:10.1137/140999335); Kumar and Saptharishi prove exponential homogeneous depth-five bounds over finite fields for a VNP family (doi:10.4230/LIPIcs.CCC.2017.31).
  • 2021/2025. Limaye, Srinivasan and Tavenas prove superpolynomial lower bounds for all constant-depth circuits, including IMM in the low-degree regime (doi:10.1145/3734215).
  • 2022–2024. Bhargav–Dutta–Saxena (doi:10.4230/LIPIcs.MFCS.2022.18), Amireddy–Garg–Kayal–Saha–Thankey (doi:10.4230/LIPIcs.ICALP.2023.12) and Forbes (doi:10.4230/LIPIcs.CCC.2024.31) improve exponents or extend fields, in regimes with dd small relative to ww.

These results either restrict the bottom linear forms, use a different width–degree regime, or concern a different polynomial. The source of this mission, an OpenAI preprint dated September 25, 2026, claims the sharp nΘ(n)n^{\Theta(\sqrt n)} bound in the balanced regime w=d=nw=d=n with unrestricted bottom forms.

Setting

An arithmetic circuit over a field KK is a finite DAG whose leaves are variables or field elements; sum gates take KK-linear combinations of their inputs, product gates multiply their inputs (with multiplicity). A ΣΠΣΠΣ\Sigma\Pi\Sigma\Pi\Sigma circuit has five layers of types +,×,+,×,++,\times,+,\times,+ from the output down, with a single output gate; edges join consecutive layers and bottom sums read leaves. Fan-in, fan-out and sharing are unrestricted, and bottom linear forms may involve any number of variables. The circuit is syntactically homogeneous if, with variables of degree 11, constants of degree 00 and product degrees adding, every sum gate has all inputs of the same formal degree. Size is the number of vertices, leaves included. The target is IMMn,n\mathrm{IMM}_{n,n}, of degree nn in n3n^3 variables.

Formalization targets

Goal: Theorem 1.1, Corollary 6.1 and Proposition 6.2

There is n0n_0 such that for all n≥n0n\ge n_0, every syntactically homogeneous ΣΠΣΠΣ\Sigma\Pi\Sigma\Pi\Sigma circuit computing IMMn,n\mathrm{IMM}_{n,n} over C\mathbb C, and more generally over any field of characteristic zero, has

size ≥ nn/400.\text{size}\ \ge\ n^{\sqrt n/400}.

Conversely, over every field and for every n≥2n\ge2 there is such a circuit with

size ≤ 2n3+rn2+rnt+1+nr−1+1 ≤ nn+4,t=⌈n⌉, r=⌈n/t⌉.\text{size}\ \le\ 2n^3+rn^2+rn^{t+1}+n^{r-1}+1\ \le\ n^{\sqrt n+4},\qquad t=\lceil\sqrt n\rceil,\ r=\lceil n/t\rceil.

The Lean statement OAI.Problem335.main bundles the three clauses and is open on the platform. The constant 1/4001/400 is the paper's and is not optimized.

Significance

The theorem determines the size of homogeneous depth-five circuits for IMMn,n\mathrm{IMM}_{n,n} up to the constant in the exponent: nΘ(n)n^{\Theta(\sqrt n)}. It removes the bottom-support restriction of Bera–Chakrabarti and works at the balanced width–degree point w=d=nw=d=n, where the shifted-partials bounds of Amireddy et al. and the low-degree results of Limaye–Srinivasan–Tavenas do not apply directly. It answers the depth-five instance of the Nisan–Wigderson question for an explicit polynomial in VP. It does not give superpolynomial bounds for general circuits.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The upper-bound clause is elementary and a natural first formal target; the lower bound requires a new rank measure and its estimates.

Difficulty

Depth-five circuits with unrestricted bottom linear forms can use linear forms involving all n3n^3 variables, which defeats measures that rely on bottom forms having small support (the Bera–Chakrabarti approach) or on set-multilinearization with degree-dependent losses (which are too costly when d=wd=w). Partial-derivative and shifted-partial measures applied directly give bounds that degrade with the bottom fan-in. One needs a measure that is small for every product of homogeneous low-degree polynomials of arbitrary support and large for IMMn,n\mathrm{IMM}_{n,n}.

Formalization scope

  • Depth5Circuit K n stores the leaves (D5Leaf: a scalar or a variable index in Fin n × Fin n × Fin n), bottom sums (lists of coefficient–leaf pairs), lower products (lists of bottom gates), middle sums, upper products, and one output sum, with explicit formal degrees and homogeneity constraints at every sum gate; empty sums have degree 00.
  • circuitSize counts leaves plus all gates plus the output gate; circuitValue evaluates to an MvPolynomial.
  • imm K n is the (0,0)(0,0) entry of the ordered product of the nn matrices Xij(t)X^{(t)}_{ij}.
  • The lower bound is stated over ℂ and, with a threshold chosen before the field, over every Field with CharZero; the upper bound over every Field, with the explicit upperGateBound.

A complete development needs multivariate polynomial algebra, the derivative-multiplication operator g[k,m](∂V,U)g_{[k,m]}(\partial_V,U) and its rank, an integral (Bargmann–Fock type) moment estimate over C\mathbb C, and a transfer to characteristic zero via integer minors. Contributions formalizing Proposition 6.2 (the upper bound) and Proposition 3.1 (the circuit-side rank bound) are welcome.

Selected references

2 thms1 active userReviewed
Mathematical LogicTheoretical Computer Science·Captain: wurtle

Generalized Star Height at Most ThreeResearch Paper

Motivation: how many nested stars does a regular language need?

A regular expression describes a set of words using letters, union, concatenation and the Kleene star P∗P^* (any finite repetition of words from PP). The star height of an expression is the depth of nesting of its stars, and it measures how many layers of unbounded repetition a regular language genuinely needs. For ordinary expressions this hierarchy is infinite. Allowing complement as an additional operation changes the picture: Boolean conditions can replace some layers of repetition, and the generalized star-height problem asks how far this goes. Whether every regular language has generalized star height at most some fixed number — and in particular whether one star always suffices — has been one of the longest-standing questions in the algebraic theory of automata.

Timeline

  • 1963 — Eggan connects ordinary star height with the cycle structure of transition graphs and raises the question of its unboundedness (Michigan Math. J. 1963).
  • 1965 — Schützenberger characterizes the star-free languages (generalized height 00) as those recognized by finite aperiodic monoids (Inform. Control 1965).
  • 1966 — Dejean and Schützenberger show that ordinary star height is unbounded already over a two-letter alphabet (Inform. Control 1966).
  • 1992 — Pin, Straubing and Thérien prove generalized height at most one for languages recognized by finite nilpotent groups of class two and for further monoid classes (Inform. Comput. 1992, Theorems 7.3 and 7.8).
  • 2002 — Straubing distinguishes the questions "is generalized star height bounded?" and "is it at most one?" in his account of the problem (LATIN 2002, p. 537).
  • 2016–2017 — Bourne and Ruškuc prove height-one bounds for subword-counting languages with factors of length at most three (Theor. Comput. Sci. 2016); Bourne extends this to arbitrary fixed factors in his thesis (St Andrews, 2017, hdl:10023/12024).
  • 2026 — Companion OpenAI preprints prove uniform bounds of thirteen (Finite Monoid Computations and a Uniform Generalized Star-Height Bound) and four (Generalized Star Height at Most Four).
  • 2026 — The OpenAI preprint Generalized Star Height at Most Three (OpenAI Math Release, September 25, 2026) claims the bound three. It has not been peer reviewed and its theorem is not formally verified. Whether height one always suffices remains open; no language of generalized height greater than one is known.

Setting

Fix a finite alphabet Σ\Sigma and let Σ∗\Sigma^* be the set of finite words. A generalized regular expression over Σ\Sigma is built from the constants 00 (denoting ∅\emptyset) and 11 (denoting {ε}\{\varepsilon\}), single letters a∈Σa\in\Sigma, union P∪QP\cup Q, concatenation PQPQ, complement ¬P\neg P (taken in Σ∗\Sigma^*), and star P∗P^*. Its height is defined by

h(0)=h(1)=h(a)=0,h(P∪Q)=h(PQ)=max⁡{h(P),h(Q)},h(¬P)=h(P),h(P∗)=1+h(P).h(0)=h(1)=h(a)=0,\quad h(P\cup Q)=h(PQ)=\max\{h(P),h(Q)\},\quad h(\neg P)=h(P),\quad h(P^*)=1+h(P).

For a regular language L⊆Σ∗L\subseteq\Sigma^*, the generalized star height hΣ(L)h_\Sigma(L) is the least height of an expression over Σ\Sigma denoting LL.

In Lean (namespace OAI.GeneralizedStarHeight), expressions are an inductive type Expression Alphabet with exactly these seven constructors, Expression.language interprets them in Mathlib's Language Alphabet (complement is Language complement, i.e. relative to all words), Expression.height is the recursion above, and HasHeightAtMost L n means some expression has language LL and height at most nn.

Formalization targets

Goal: generalized star height at most three (Theorem 1.1)

For every finite alphabet Σ\Sigma and every regular language L⊆Σ∗L\subseteq\Sigma^*,

hΣ(L)≤3.h_\Sigma(L)\le 3 .

The goal is published on the platform with status Open.

Significance

The result itself. Before 2026 it was not known whether generalized star height is bounded at all; all positive results covered restricted families of monoids or languages. Theorem 1.1 gives a uniform bound independent of the alphabet and of the recognizing automaton, settling the boundedness question. It leaves open the sharper question of whether height one always suffices: no language is known to require height two. A uniform bound also implies that the hierarchy of generalized heights has at most four nonempty levels, which narrows where any separating example must be sought.

Formalizing it. The statement is short and fully elementary, but the proof composes many constructions (finite-monoid recognition, prefix codes of episodes, split identities, marker scales) whose height accounting is error-prone. A formal proof would certify the boundedness theorem itself. Mathlib already has regular languages (Language.IsRegular) and ordinary regular expressions; this mission adds generalized expressions with complement and their height.

Difficulty

The classical lower bounds for ordinary star height do not transfer once complement is allowed, and complement can simulate many but not obviously all counting arguments. The natural approach — write each fiber of a morphism from Σ∗\Sigma^* to a finite monoid by an expression that simulates the monoid computation letter by letter — needs one star per level of the computation's dependence on earlier history, and the depth of this dependence grows with the monoid. Group components are the difficulty: aperiodic monoids give height zero, but counting modulo nn and nonabelian group computations require stars, and a uniform bound must handle arbitrary finite groups nested inside arbitrary monoids without the number of stars growing with their size.

Formalization scope

  • The alphabet is any Type u with [Finite Alphabet]; regularity is Mathlib's Language.IsRegular (acceptance by a finite-state DFA).
  • Expressions must use letters of the same alphabet, so no auxiliary letters may be introduced; complement is relative to all words over that alphabet.
  • height charges 11 only for stars; complement, union and concatenation are free, exactly as in the source. Since HasHeightAtMost asks only for existence of an expression, no bound on expression size or computability is claimed, matching the source's remark that the construction bounds nesting only.
  • Needed infrastructure: recognition of regular languages by finite monoids, prefix codes and unique factorization, and closure of bounded-height expressions under Boolean operations. The generalized-expression layer is reusable for the companion bounds (four and thirteen) and for formal work on star-free languages.

Selected references

2 thms1 active userReviewed
Number TheoryTheoretical Computer Science·Captain: mikedeng1

Factoring Polynomials with Rational Coefficients III: A Reduced Basis of the Lattice of Multiples of h mod p^k Finds the Irreducible Factor h₀ = gcd(b₁, …, b_t)Research Paper

Motivation

Factoring a polynomial with rational coefficients into irreducible factors is one of the basic tasks of computer algebra. Before 1982 the standard method (Berlekamp's algorithm modulo a small prime, Hensel lifting, then recombination of the pp-adic factors, as in Zassenhaus's approach) could take exponential time, because the number of ways to recombine modular factors grows exponentially with the number of factors. A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász gave the first deterministic polynomial-time algorithm for factoring primitive polynomials in Z[X]\mathbb Z[X] (Math. Ann. 261, 1982). Its key idea is to replace recombination by a search for a short vector in a lattice, and the lattice basis reduction algorithm introduced for that purpose (the LLL algorithm) has since become a standard tool in number theory, cryptanalysis and integer programming.

Section 2 of the paper, Factors and Lattices, is the bridge between the two halves: it shows that an irreducible factor of ff can be read off from a reduced basis of a lattice built from a pp-adic factor of ff. This mission formalizes that section.

Timeline. Mignotte (1974) bounded the coefficients of a factor of an integer polynomial in terms of the polynomial itself. A. K. Lenstra (Mathematisch Centrum report IW 190/81, 1981, Theorem 2) proved the weaker statement that, under the same conditions, a short lattice vector has a nontrivial gcd with ff. LLL (1982) proved the sharper Propositions (2.7), (2.13) and (2.16) used here, which pin down the irreducible factor h0h_0 itself.

Setting

For g=∑iaiXig=\sum_i a_iX^i with real coefficients, the length of gg is ∣g∣=(∑iai2)1/2|g|=(\sum_i a_i^2)^{1/2}. For a positive integer qq, (g mod q)(g\bmod q) is the polynomial over Z/qZ\mathbb Z/q\mathbb Z obtained by reducing every coefficient modulo qq.

Throughout, pp is a prime number, kk a positive integer, and f∈Z[X]f\in\mathbb Z[X] a polynomial of degree n>0n>0. A polynomial h∈Z[X]h\in\mathbb Z[X] is fixed with

  • (2.1) hh has leading coefficient 11;
  • (2.2) (h mod pk)(h\bmod p^k) divides (f mod pk)(f\bmod p^k) in (Z/pkZ)[X](\mathbb Z/p^k\mathbb Z)[X];
  • (2.3) (h mod p)(h\bmod p) is irreducible in Fp[X]\mathbb F_p[X];
  • (2.4) (h mod p)2(h\bmod p)^2 does not divide (f mod p)(f\bmod p) in Fp[X]\mathbb F_p[X].

Write l=deg⁡hl=\deg h, so 0<l≤n0<l\le n. Proposition (2.5) shows that ff has an irreducible factor h0∈Z[X]h_0\in\mathbb Z[X] with (h mod p)∣(h0 mod p)(h\bmod p)\mid(h_0\bmod p), unique up to sign; this is the factor the section recovers.

Fix an integer m≥lm\ge l. The lattice LL is the set of polynomials g∈Z[X]g\in\mathbb Z[X] of degree at most mm such that (h mod pk)(h\bmod p^k) divides (g mod pk)(g\bmod p^k). Identifying ∑i=0maiXi\sum_{i=0}^m a_iX^i with (a0,…,am)∈Rm+1(a_0,\dots,a_m)\in\mathbb R^{m+1}, LL is a lattice of rank m+1m+1 with basis {pkXi:0≤i<l}∪{hXj:0≤j≤m−l}\{p^kX^i:0\le i<l\}\cup\{hX^j:0\le j\le m-l\} and determinant pklp^{kl}.

A basis b1,…,bm+1b_1,\dots,b_{m+1} of LL is reduced if its Gram–Schmidt data bi∗b_i^*, μij=(bi,bj∗)/(bj∗,bj∗)\mu_{ij}=(b_i,b_j^*)/(b_j^*,b_j^*) satisfy ∣μij∣≤12|\mu_{ij}|\le\frac12 for j<ij<i and ∣bi∗+μi i−1bi−1∗∣2≥34∣bi−1∗∣2|b_i^*+\mu_{i\,i-1}b_{i-1}^*|^2\ge\frac34|b_{i-1}^*|^2 for 1<i≤m+11<i\le m+1.

Formalization targets

Goal: Proposition (2.16)

Assume

(2.14)pkl>2mn/2(2mm)n/2∣f∣m+n,\text{(2.14)}\qquad p^{kl}>2^{mn/2}\binom{2m}{m}^{n/2}|f|^{m+n},

that b1,…,bm+1b_1,\dots,b_{m+1} is a reduced basis of LL, and that some jj satisfies

(2.17)∣bj∣<(pkl/∣f∣m)1/n.\text{(2.17)}\qquad |b_j|<\big(p^{kl}/|f|^m\big)^{1/n}.

If tt is the largest such jj, then

deg⁡h0=m+1−t,h0=gcd⁡(b1,…,bt),\deg h_0=m+1-t,\qquad h_0=\gcd(b_1,\dots,b_t),

and (2.17) holds for all 1≤j≤t1\le j\le t.

Milestones

  1. (2.5): existence and uniqueness of h0h_0, and for g∣fg\mid f the equivalence of (h mod p)∣(g mod p)(h\bmod p)\mid(g\bmod p), (h mod pk)∣(g mod pk)(h\bmod p^k)\mid(g\bmod p^k) and h0∣gh_0\mid g.
  2. (2.11): inside the proof of (2.7), the elements of M={λf+μb}M=\{\lambda f+\mu b\} of degree below e+le+l lie in pkZ[X]p^k\mathbb Z[X].
  3. (2.7): if b∈Lb\in L and pkl>∣f∣m∣b∣np^{kl}>|f|^m|b|^n then h0∣bh_0\mid b.
  4. Mignotte's bound: a divisor gg of ff with deg⁡g≤m\deg g\le m has ∣g∣≤(2mm)1/2∣f∣|g|\le\binom{2m}{m}^{1/2}|f|.
  5. (2.13): under (2.14), deg⁡h0≤m\deg h_0\le m if and only if ∣b1∣<(pkl/∣f∣m)1/n|b_1|<(p^{kl}/|f|^m)^{1/n}.
  6. (2.18): #J≤m+1−deg⁡h1\#J\le m+1-\deg h_1 for linearly independent bjb_j divisible by h1h_1.
  7. (2.19): if deg⁡h0≤m\deg h_0\le m, then {1,…,m+1−deg⁡h0}⊂J\{1,\dots,m+1-\deg h_0\}\subset J.

Companion items: the basis of LL and d(L)=pkld(L)=p^{kl} (2.6), and the remark that for t=1t=1 the vector b1b_1 is itself an irreducible factor of ff.

Significance

Proposition (2.16) is what makes the factoring algorithm of Sect. 3 correct: running the reduction for increasing mm, the first mm for which (2.15) holds produces h0h_0 by one gcd computation, and repeating on f/h0f/h_0 factors ff completely. Together with the polynomial running time of basis reduction (missions I and II of this series), it yields the polynomial-time factoring theorem (3.6). Proposition (2.7) on its own is a general principle, often reused: a polynomial that is divisible by hh modulo pkp^k and has small norm relative to pklp^{kl} must share the factor h0h_0 with ff.

All results here are proved in the paper and standard in textbooks (e.g. von zur Gathen and Gerhard, Modern Computer Algebra). To our knowledge there is no machine-checked proof of (2.7), (2.13) or (2.16) in Lean or Mathlib. Mathlib has Hensel-type lemmas and the Mahler measure, including a coefficient-wise Mignotte bound and Landau's inequality, but not the ℓ2\ell^2 form of Mignotte's bound used here, nor any of the lattice statements. A Lean development of this section would be the algebraic core of a verified LLL factoring theorem.

Difficulty

The obvious argument for (2.7) is to bound the resultant of ff and bb: it is divisible by pklp^{kl} when they share a factor modulo pkp^k, and bounded by ∣f∣m∣b∣n|f|^m|b|^n by Hadamard. That argument gives only gcd⁡(f,b)≠1\gcd(f,b)\ne1, the weaker version of [8], not that h0h_0 divides bb. The paper's sharper statement needs a lattice MM of combinations λf+μb\lambda f+\mu b, the projection to its top coefficients, and the congruence argument (2.11) that forces the low-degree elements of MM into pkZ[X]p^k\mathbb Z[X]; formalizing it requires determinant and Hadamard bounds for a lattice of rank n+m′−2en+m'-2e inside a space of polynomials.

Mignotte's ℓ2\ell^2 bound needs the Mahler measure and the inequality ∣g∣≤(2dd)1/2M(g)|g|\le\binom{2d}{d}^{1/2}M(g), which is not the coefficient-wise form available in Mathlib. The step (2.19) needs Proposition (1.12) on reduced bases, which is the goal of mission I. The final part of (2.16) needs the primitivity of the basis vectors, which depends on LL being exactly the set of multiples of hh modulo pkp^k of degree at most mm.

Formalization scope

Polynomials are Polynomial ℤ; (g mod q)(g\bmod q) is g.map (Int.castRingHom (ZMod q)); ∣g∣|g| is the square root of the sum of the squares of the coefficients over the support. Degrees are natDegree, except in (2.11), where degree with values in WithBot ℕ keeps deg⁡0=−∞\deg 0=-\infty as on the page. A polynomial of degree at most mm is identified with its coefficient vector in EuclideanSpace ℝ (Fin (m + 1)). Linear independence of b1,…,bm+1b_1,\dots,b_{m+1} is over R\mathbb R on coefficient vectors; "basis for LL" means in LL, independent, and spanning LL over Z\mathbb Z. Gram–Schmidt vectors are Mathlib's unnormalised InnerProductSpace.gramSchmidt.

Indices are 0-based: the paper's b1b_1 is b 0. The index tt of (2.16) is kept as the paper's 1-based value, 1≤t≤m+11\le t\le m+1, so deg⁡h0=m+1−t\deg h_0=m+1-t appears unchanged. The powers 2mn/22^{mn/2}, (2mm)n/2\binom{2m}{m}^{n/2}, (2mm)1/2\binom{2m}{m}^{1/2} and (⋅)1/n(\cdot)^{1/n} are real powers with real exponents.

The standing assumptions are hypotheses of every item that involves pp, kk or hh: pp prime, k≥1k\ge1, deg⁡f>0\deg f>0, (2.1)–(2.4), m≥lm\ge l. Mignotte's bound (which assumes only f≠0f\ne0) and (2.18) (pure linear algebra on polynomials of degree at most mm) do not need them. The factor h0h_0 is any irreducible h0∈Z[X]h_0\in\mathbb Z[X] with h0∣fh_0\mid f and (h mod p)∣(h0 mod p)(h\bmod p)\mid(h_0\bmod p). A gcd is stated by its universal property (divides each, and every common divisor divides it), which determines it up to sign. Two milestones are stated slightly more generally than the page: Mignotte's bound for every divisor of degree at most mm, and (2.18) for every nonzero common divisor h1h_1.

The goal does not assume (2.7), (2.13), Mignotte's bound, (2.18) or (2.19); these are milestones. A trivial formalization in which h0h_0 is an arbitrary divisor of ff, or in which "reduced basis" is asserted of a family that need not be a basis of LL, is ruled out by the definitions.

Needed infrastructure: Hensel-type arguments over Z/pkZ\mathbb Z/p^k\mathbb Z, Gauss's lemma, the Mahler measure, Hadamard's inequality, and Proposition (1.12) on reduced bases. The lattice determinant results and the ℓ2\ell^2 Mignotte bound are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the missing Mathlib infrastructure.

Selected references

  • A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Math. Ann. 261 (1982), 515–534. https://doi.org/10.1007/BF01457454
  • M. Mignotte, An inequality about factors of polynomials, Math. Comp. 28 (1974), 1153–1157 (reference [10] of the paper).
  • D. E. Knuth, The Art of Computer Programming, Vol. 2, Seminumerical Algorithms, Addison-Wesley, 1981, Exercise 4.6.2.20 (reference [7] of the paper).
  • A. K. Lenstra, Lattices and factorization of polynomials, Report IW 190/81, Mathematisch Centrum, Amsterdam, 1981 (reference [8] of the paper; its Theorem 2 is the weaker form of (2.7)).
  • J. von zur Gathen, J. Gerhard, Modern Computer Algebra, 3rd ed., Cambridge University Press, 2013, Ch. 16 (textbook treatment).
9 thms1 active userReviewed
Algebraic GeometryAnalysisPure Mathematics·Captain: mikedeng1

Tasty Bits of Several Complex Variables IX: Weierstrass Preparation and the Ring of GermsTextbook

Why the ring of germs

Local complex analytic geometry studies zero sets of holomorphic functions near a point. The natural algebraic object for this is the ring of germs Op\mathcal{O}_p of holomorphic functions at p∈Cnp \in \mathbb{C}^n: two functions are identified if they agree near pp. The ring Op\mathcal{O}_p is the local ring of the complex manifold Cn\mathbb{C}^n at pp in the sense of analytic geometry; its algebraic properties (Noetherian, integral domain, unique factorization) are what make the local theory of analytic varieties, their irreducible components and their singular sets work. This mission formalizes the section of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (jirka.org/scv) that establishes these properties, together with the two tools they rest on, the Weierstrass preparation and division theorems.

The preparation theorem goes back to Weierstrass (published 1886). Rückert (1933) used preparation and division to prove that the ring of convergent power series is Noetherian, the starting point of the algebraic treatment of local analytic geometry.

Setting

A point of Cn\mathbb{C}^n is z=(z1,…,zn)z = (z_1, \dots, z_n); when a last variable is singled out, z=(z′,zn)z = (z', z_n) with z′∈Cn−1z' \in \mathbb{C}^{n-1}. A function on an open set is holomorphic if it is complex differentiable there; O(U)\mathcal{O}(U) is the set of holomorphic functions on UU. A domain is a nonempty connected open set.

A germ at pp is an equivalence class of functions defined on neighborhoods of pp, two functions being equivalent if they agree on some neighborhood of pp. Germs of complex-valued functions form a commutative ring under pointwise operations of representatives. The ring of germs of holomorphic functions Op=nOp\mathcal{O}_p = {}_n\mathcal{O}_p consists of the germs having a representative holomorphic on a neighborhood of pp.

For ff holomorphic near pp, write f(z)=∑kfk(z−p)f(z) = \sum_k f_k(z - p) with fkf_k homogeneous of degree kk. The order of vanishing ord⁡pf\operatorname{ord}_p f is the least kk with fk≢0f_k \not\equiv 0, and ∞\infty if f≡0f \equiv 0.

A Weierstrass polynomial of degree k≥0k \ge 0 on an open U∋0U \ni 0 in Cn−1\mathbb{C}^{n-1} is a monic polynomial in znz_n,

P(z′,zn)=znk+∑ℓ=0k−1cℓ(z′) znℓ,P(z', z_n) = z_n^k + \sum_{\ell=0}^{k-1} c_\ell(z')\, z_n^\ell,

with coefficients cℓc_\ell holomorphic on UU and cℓ(0)=0c_\ell(0) = 0. A polydisc is a product of open discs. For a fixed z′z', zeros of zn↦f(z′,zn)z_n \mapsto f(z', z_n) are geometrically distinct if they are distinct points; a zero is geometrically unique if it is the only one.

Formalization targets

Goal: Theorem 6.4.2

For every nn and p∈Cnp \in \mathbb{C}^n,

Op is a unique factorization domain:\mathcal{O}_p \text{ is a unique factorization domain:}

it is an integral domain, and up to multiplication by units and permutation every nonzero nonunit has a unique factorization into irreducible elements of Op\mathcal{O}_p.

Milestones

In attack order:

  1. Theorem 6.2.3 (Weierstrass preparation). If f∈O(U)f \in \mathcal{O}(U), 0∈U0 \in U, f(0)=0f(0) = 0, and zn↦f(0,zn)z_n \mapsto f(0, z_n) has order of vanishing k≥1k \ge 1 at 00, then on some open polydisc V=V′×DV = V' \times D with 0∈V⊂U0 \in V \subset U,
f(z′,zn)=u(z′,zn) P(z′,zn)f(z', z_n) = u(z', z_n)\, P(z', z_n)

with u∈O(V)u \in \mathcal{O}(V) nowhere zero and PP a Weierstrass polynomial of degree kk with coefficients holomorphic in V′V' whose zeros in znz_n lie in DD for all z′∈V′z' \in V'; uu and PP are unique. 2. Theorem 6.2.5 (Weierstrass division). For ff holomorphic near 00 and PP a Weierstrass polynomial of degree k≥1k \ge 1, there are a neighborhood VV of 00 and unique q,r∈O(V)q, r \in \mathcal{O}(V), rr a polynomial in znz_n of degree less than kk, with f=qP+rf = qP + r on VV. 3. Proposition 6.3.1. On domains U′×DU' \times D, if for every z′∈U′z' \in U' the function zn↦f(z′,zn)z_n \mapsto f(z', z_n) has a geometrically unique zero α(z′)∈D\alpha(z') \in D, then α\alpha is holomorphic in U′U'. 4. Theorem 6.3.3 (discriminant). For DD a bounded domain, U′U' a domain, f∈O(U′×D)f \in \mathcal{O}(U' \times D) whose zero set has no limit points on U′×∂DU' \times \partial D, there are mm and a holomorphic Δ≢0\Delta \not\equiv 0 on U′U' such that zn↦f(z′,zn)z_n \mapsto f(z', z_n) has exactly mm geometrically distinct zeros in DD for Δ(z′)≠0\Delta(z') \ne 0 and fewer than mm for Δ(z′)=0\Delta(z') = 0. 5. Theorem 6.4.1. Op\mathcal{O}_p is Noetherian.

Significance

The preparation theorem reduces a holomorphic function near a point, after a unit, to a polynomial in one variable over the ring of functions of the others; the division theorem is division with remainder by such a polynomial. Together they turn O0\mathcal{O}_0 in nn variables into an object controlled by the polynomial ring O0[zn]\mathcal{O}_0[z_n] in n−1n - 1 variables, and that is how both the Noetherian property and unique factorization are proved. Unique factorization gives the decomposition of a germ of a hypersurface into irreducible components; the Noetherian property says that every germ of an analytic variety is cut out by finitely many functions. Proposition 6.3.1 and Theorem 6.3.3 describe how the zeros of zn↦f(z′,zn)z_n \mapsto f(z', z_n) move with z′z', the input to the study of hypervarieties in the following sections.

The results are classical. The book proves them, leaving some steps as exercises: uniqueness in the division theorem (Exercise 6.2.10), the one-variable cases of 6.4.1 and 6.4.2 (Exercises 6.4.2, 6.4.6), and the irreducibility step in 6.4.2 (Exercise 6.4.7). Mathlib has the algebra (Noetherian rings, unique factorization monoids, Hilbert's basis theorem, the Gauss lemma for polynomial rings), germs along filters, and one-variable complex analysis. The platform has the Weierstrass preparation and division theorems for formal power series over complete local rings. None of the statements of this mission about convergent germs and holomorphic functions has a machine-checked proof.

Difficulty

The statements concern convergent objects, and the algebra alone does not see convergence. The formal preparation and division theorems produce a factorization or a quotient as formal power series; they do not say that the output converges, nor that it is holomorphic on a fixed neighborhood, nor where the zeros of the Weierstrass polynomial lie. Likewise, the formal power series ring is known to be a Noetherian UFD, but Op\mathcal{O}_p is a proper subring and neither property passes to subrings. The coefficients of the Weierstrass polynomial are built from the zeros of zn↦f(z′,zn)z_n \mapsto f(z', z_n), which in general cannot be chosen continuously in z′z' (the two square roots of z1z_1 already show this), so the holomorphy of the coefficients cannot come from the zeros one at a time.

For the goal, the induction on nn requires identifying O0\mathcal{O}_0 in n−1n - 1 variables, its polynomial ring, and a subring of O0\mathcal{O}_0 in nn variables, and moving between germs and representatives on explicit neighborhoods. A linear change of coordinates is needed to reach the hypothesis of the preparation theorem, so invariance of Op\mathcal{O}_p under such changes is also part of the work.

Formalization scope

  • Cn\mathbb{C}^n is Fin n → ℂ; where a last variable is singled out, Cn−1×C\mathbb{C}^{n-1} \times \mathbb{C} is (Fin d → ℂ) × ℂ with d=n−1d = n - 1, so d=0d = 0 is the case n=1n = 1. Holomorphic on an open set is DifferentiableOn ℂ, which agrees with the book's Definition 1.1.2 on open sets.
  • Op\mathcal{O}_p is GermRing n p: the subring of Mathlib's germ ring (𝓝 p).Germ ℂ of germs with a representative complex-differentiable at every point near pp. The goal produces the IsDomain structure and asserts UniqueFactorizationMonoid; Theorem 6.4.1 is IsNoetherianRing.
  • Ruled out: replacing Op\mathcal{O}_p by the ring of all germs of functions (not a domain) or by formal power series MvPowerSeries (Fin n) ℂ. Both change the theorem; convergence is the whole point.
  • The order of vanishing is ℕ∞-valued: the least kk with nonzero kk-th derivative at pp, and ∞\infty if there is none.
  • A Weierstrass polynomial is given by its coefficient tuple c0,…,ck−1c_0, \dots, c_{k-1}; the polydisc V′×DV' \times D of Theorem 6.2.3 is a coordinatewise polydisc with positive radii times an open disc, both centers arbitrary as in the book. "All kk zeros lie in DD" is stated as "every zero lies in DD", equivalent for a monic polynomial of degree kk. Uniqueness in 6.2.3 and 6.2.5 is uniqueness on the VV produced.
  • In Theorem 6.3.3 zeros are counted as distinct points with Set.encard. The book writes m∈Nm \in \mathbb{N} with N={1,2,… }\mathbb{N} = \{1, 2, \dots\}; the statement allows m=0m = 0, since for ff without zeros no m≥1m \ge 1 can satisfy the conclusion.

A complete development needs the one-variable argument principle and Cauchy integral formula with holomorphic parameters, Newton's identities, Radó's theorem (for 6.3.3), Hilbert's basis theorem and the Gauss lemma (in Mathlib), and the identification of O0\mathcal{O}_0 in n−1n - 1 variables with a subring of O0\mathcal{O}_0 in nn variables. A general API for rings of holomorphic germs and their changes of coordinates is reusable in the next mission of this series (hypervarieties and their singular sets); contributions of it as standalone lemmas are welcome.

Selected references

  • J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, Chapter 6, §§6.1–6.4. https://www.jirka.org/scv/scv.pdf
  • W. Rückert, "Zum Eliminationsproblem der Potenzreihenideale", Mathematische Annalen 107 (1933).
  • R. C. Gunning and H. Rossi, Analytic Functions of Several Complex Variables, Prentice-Hall, 1965; reprint AMS Chelsea, 2009, Chapter II.
10 thms1 active userReviewed
Completed
AnalysisNumber Theory·Captain: lisamegawatts

Lindemann–Weierstrass I: Exponential IndependenceResearch Paper

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 ee 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 ee 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 Q‾⊂C\overline{\mathbb Q}\subset\mathbb C for the field of algebraic complex numbers and exp⁡(z)=ez\exp(z)=e^z for the complex exponential.

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

The strongest target uses natural-number linear independence of (ui)(u_i): distinct finitely supported tuples of natural coefficients give distinct sums ∑iniui\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 (ui)(u_i),

{eui:i∈I} is linearly independent over Q‾.\{e^{u_i}:i\in I\}\text{ is linearly independent over }\overline{\mathbb Q}.

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

Hermite–Lindemann and classical constants

For every nonzero algebraic a∈Ca\in\mathbb C,

ea is transcendental.e^a\text{ is transcendental}.

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

Integer winding consumer

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

(eiαw(j))j∈I linearly independent over Q‾.\bigl(e^{i\alpha w(j)}\bigr)_{j\in I}\text{ linearly independent over }\overline{\mathbb Q}.

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 (ui)(u_i) is a natural-number-linearly-independent family in Q‾\overline{\mathbb Q}, then

{eui:i∈I} is algebraically independent over Q‾.\{e^{u_i}:i\in I\}\text{ is algebraically independent over }\overline{\mathbb Q}.

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 ex+y=exeye^{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 aa produces the two-sided phase family (ena)n∈Z(e^{na})_{n\in\mathbb Z}; after a Laurent-polynomial shift, the theorem makes distinct integer labels linearly independent over Q‾\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 Q‾\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 Q\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≠0a\ne0 in Hermite–Lindemann is load-bearing: e0=1e^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

12 thms1 active userReviewed
Completed
Captain: lisamegawatts

Grade-4 Cartan Mixing (Weinberg/Cabibbo correction)Open Problem

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.

10 thms1 active userReviewed
Completed
Number TheoryRepresentation Theory·Captain: Lucas

Ngo's Fundamental Lemma I: Discriminant, Resultant and the Transfer FactorResearch Paper

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 qq 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 GG be a split reductive group over a field with maximal torus TT, character lattice X∗(T)X^*(T), cocharacter lattice X∗(T)X_*(T), root system Φ⊂X∗(T)\Phi \subset X^*(T) and Weyl group WW. Write t\mathfrak{t} for the Cartan subalgebra, so that each root α\alpha has a differential dαd\alpha, a linear form on t\mathfrak{t}. Ngô's discriminant is the product

DG  =  ∏α∈Φdα,D_G \;=\; \prod_{\alpha \in \Phi} d\alpha ,

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

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

ΦH  =  {α∈Φ  :  κ(α∨)=1},\Phi_H \;=\; \{\alpha \in \Phi \;:\; \kappa(\alpha^\vee) = 1\} ,

with Weyl group WH⊂WW_H \subset W and its own discriminant DH=∏α∈ΦHdαD_H = \prod_{\alpha \in \Phi_H} d\alpha. Choose a subset Λ⊂Φ−ΦH\Lambda \subset \Phi - \Phi_H containing exactly one root out of each pair {α,−α}\{\alpha, -\alpha\} of opposite roots outside ΦH\Phi_H, and set

RHG  =  ∏α∈Λdα.R^G_H \;=\; \prod_{\alpha \in \Lambda} d\alpha .

Finally let FF be a non-archimedean local field with valuation vv and residue cardinality qq, and recall Ngô's normalizing factors ΔG(a)=q−v(DG(a))/2\Delta_G(a) = q^{-v(D_G(a))/2} and ΔH(aH)=q−v(DH(aH))/2\Delta_H(a_H) = q^{-v(D_H(a_H))/2}.

Formalization targets

Goal (1.11.3): the transfer factor identity

v(DG(a))  =  v(DH(aH))  +  2 v(RHG(aH))v\bigl(D_G(a)\bigr) \;=\; v\bigl(D_H(a_H)\bigr) \;+\; 2\, v\bigl(R^G_H(a_H)\bigr)

for a point aHa_H of the endoscopic Cartan with image aa. Equivalently ΔH(aH)ΔG(a)−1=q r\Delta_H(a_H)\Delta_G(a)^{-1} = q^{\,r} with r=v(RHG(aH))r = v(R^G_H(a_H)): this is exactly what lets one pass between the two forms of the fundamental lemma, Oaκ(1g)=q rSOaH(1h)O^{\kappa}_a(\mathbf{1}_{\mathfrak{g}}) = q^{\,r} SO_{a_H}(\mathbf{1}_{\mathfrak{h}}) and ΔG(a)Oaκ(1g)=ΔH(aH)SOaH(1h)\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 vv of the divisor identity ν∗DG=DH+2RHG\nu^* D_G = D_H + 2 R^G_H of 1.10.3, which in turn rests on the fact that RHGR^G_H — which depends on a choice of Λ\Lambda — is nevertheless WHW_H-invariant, and on the fact that ΦH\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 ΔG(a)Oaκ(1g,dt)=ΔH(aH)SOaH(1h,dt)\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 GG 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 Φ−ΦH\Phi - \Phi_H into pairs {α,−α}\{\alpha,-\alpha\} and collecting squares is bookkeeping; that DGD_G is WW-invariant is immediate because WW permutes Φ\Phi. The content is in Lemma 1.10.2: Λ\Lambda is not stable under WHW_H, so w∈WHw \in W_H carries ∏α∈Λdα\prod_{\alpha\in\Lambda} d\alpha to (−1)m(w)∏α∈Λdα(-1)^{m(w)} \prod_{\alpha\in\Lambda} d\alpha, where m(w)m(w) counts the roots of Λ\Lambda sent into −Λ-\Lambda; the claim is that m(w)m(w) is always even. The naive attempt — check it on the generating reflections of WHW_H — is exactly where a careless argument goes wrong, since it is false for reflections in roots outside ΦH\Phi_H. Ngô's argument identifies the sign with (−1)ℓG(w)(−1)ℓH(w)(-1)^{\ell_G(w)} (-1)^{\ell_H(w)}, the ratio of the sign characters of WW and WHW_H, and observes that both compute the determinant of ww acting on the same reflection representation.

Formalization scope

Root systems are modelled with Mathlib's RootPairing ι R M N: the module MM plays the role of X∗(T)X^*(T), the module NN the role of X∗(T)X_*(T) and of the Cartan on which the differentials dαd\alpha are evaluated, and P.root′iP.root' i is the linear form dα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 Z\mathbb{Z} coefficients as in the definition of a root datum. Products over Φ\Phi and ΦH\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)∣Λ∣(-1)^{|\Lambda|} is carried explicitly rather than discarded. Lemma 1.10.2 is stated over Q\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 Z∪{∞}\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

7 thms1 active userReviewed
Completed
Theoretical Computer Science·Captain: Cosme

Eilenberg Theorems for Many-Sorted FormationsResearch Paper

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 SS and an SS-sorted signature Σ\Sigma. For an SS-sorted set XX, write TΣ(X)T_\Sigma(X) for the free Σ\Sigma-algebra on XX. A congruence Φ\Phi on a many-sorted algebra is a family of equivalence relations Φs\Phi_s, one on each carrier sort, compatible with every basic operation. Its index is finite when the entire sorted quotient family

(TΣ(X)s/Φs)s∈S(T_\Sigma(X)_s/\Phi_s)_{s\in S}

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

A finite-index congruence formation F\mathfrak F selects, for every variable family XX, a nonempty filter F(X)\mathfrak F(X) of finite-index congruences on TΣ(X)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 L\mathcal L selects regular languages in each TΣ(X)T_\Sigma(X). It contains every language saturated by the universal congruence; whenever L,K∈L(X)L,K\in\mathcal L(X) it contains every language saturated by Ω(L)∩Ω(K)\Omega(L)\cap\Omega(K); and it satisfies the corresponding pullback-saturation condition for quotient-surjective homomorphisms.

The two constructions are

LF(X)={L∣L is saturated by some Φ∈F(X)},\mathcal L_{\mathfrak F}(X) =\{L\mid \text{$L$ is saturated by some }\Phi\in\mathfrak F(X)\},

and

FL(X)={Φ∣Φ has finite index and every Φ-saturated language lies in L(X)}. \mathfrak F_{\mathcal L}(X) =\{\Phi\mid \text{$\Phi$ has finite index and every $\Phi$-saturated language lies in $\mathcal L(X)$}\}.

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.

Form⁡Cgrfi(Σ)≅Form⁡Langr(Σ). \operatorname{Form}_{\mathrm{Cgr}_{\mathrm{fi}}}(\Sigma) \cong \operatorname{Form}_{\mathrm{Lang}_{r}}(\Sigma).

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

FLF=F,LFL=L. \mathfrak F_{\mathcal L_{\mathfrak F}}=\mathfrak F, \qquad \mathcal L_{\mathfrak F_{\mathcal L}}=\mathcal L.

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.
9 thms1 active userReviewed
Completed
Theoretical Computer Science·Captain: Cosme

A Kleene Theorem for Free Many-Sorted AlgebrasResearch Paper

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 SS. An SS-sorted set A=(As)s∈SA = (A_s)_{s\in S} is a family of sets; it is finite when ∐s∈SAs\coprod_{s\in S} A_s is finite. An SS-sorted signature Σ\Sigma assigns to each pair (s,s)∈S⋆×S(\mathbf{s}, s) \in S^\star \times S a set Σs,s\Sigma_{\mathbf{s},s} of operation symbols of arity s\mathbf{s} and coarity ss. A Σ\Sigma-algebra A\mathbf{A} is an SS-sorted set AA together with, for each σ∈Σs,s\sigma \in \Sigma_{\mathbf{s},s}, an operation σA ⁣:As→As\sigma^{\mathbf A}\colon A_{\mathbf s} \to A_s, where As=∏jAsjA_{\mathbf s} = \prod_{j} A_{s_j}. A homomorphism commutes with all operations sortwise.

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

Two operations on languages, both performed sortwise, generate the regular expressions. Given a variable z∈Xuz \in X_u and a language L⊆TΣ(X)uL \subseteq \mathrm T_\Sigma(X)_u, zz-substitution ( ⁣zL ⁣)s♯p\left(\!\begin{smallmatrix}z\\ L\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s replaces, in every term of an input language of sort ss, each occurrence of zz independently by a term of LL. The zz-iteration is L⋆z=⋃i∈NLi zL^{\star z} = \bigcup_{i\in\mathbb N} L^{i\,z}, where L0 z={z}L^{0\,z} = \{z\} and Li+1 z=Li z∪( ⁣zLiz ⁣)s♯p(L)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 SS-sorted set ZZ, the regular signature Reg(S,Σ,Z)\mathrm{Reg}(S,\Sigma,Z) expands Σ\Sigma by an empty constant ∅s\varnothing_s, a binary sum +s+_s, a unary zz-iteration (⋅)⋆z(\cdot)^{\star z} for each z∈Zsz\in Z_s, and a zz-substitution operation for each z∈Ztz\in Z_t. Its terms are the regular expressions over (S,Σ,Z)(S,\Sigma,Z); the power algebra TΣ(Z)℘\mathbf T_\Sigma(Z)^\wp carries a canonical Reg(S,Σ,Z)\mathrm{Reg}(S,\Sigma,Z)-algebra structure, and interpreting a regular expression there yields a language {R}sZ♯\{R\}^{Z\sharp}_s. A language L⊆TΣ(X)sL\subseteq \mathrm T_\Sigma(X)_s is ss-regular when L={R}sZ♯L = \{R\}^{Z\sharp}_s for some finite Z⊇XZ\supseteq X and some regular expression RR of type ss; write Regs(TΣ(X))\mathrm{Reg}_s(\mathbf T_\Sigma(X)).

Formalization targets

Goal — the many-sorted Kleene theorem

∀ s∈S,Recs(TΣ(X))  =  Regs(TΣ(X)).\forall\, s\in S,\qquad \mathrm{Rec}_s(\mathbf T_\Sigma(X)) \;=\; \mathrm{Reg}_s(\mathbf T_\Sigma(X)).

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 SS, every finite SS-sorted signature Σ\Sigma, and every finite SS-sorted set XX. It splits into Regs⊆Recs\mathrm{Reg}_s \subseteq \mathrm{Rec}_s (Corollary 4.8) and Recs⊆Regs\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 Reg\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 SS-sorted family K≤NK \le N recording, for each sort tt, the set KtK_t of state values still admissible at internal subterms. The induction is on ∥∥K∥∥=∑s∈Sks\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 Lu(C,K,l)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: SS a type with [Fintype S]; an SS-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-ss carrier Set (T_Σ Z s); ss-recognizability as the existence of a finite Σ\Sigma-algebra, a homomorphism, and a subset whose sortwise preimage is the language. Committed conventions: SS finite throughout; Σ\Sigma finite and XX 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 {∅,+,(⋅)⋆z,z-subst}\{\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 ss-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.
32 thms1 active userReviewed
Completed
Number Theory·Captain: tomasz

Senthil Kumar: Weierstrass elliptic and zeta valuesResearch Paper

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 ω1,ω2\omega_1,\omega_2 that are linearly independent over the real numbers. Their integer linear combinations form the period lattice

Ω=Zω1+Zω2.\Omega=\mathbb Z\omega_1+\mathbb Z\omega_2.

The formal representation is Mathlib's PeriodPair. Its lattice determines the Weierstrass elliptic function ℘\wp and invariants g2,g3g_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

ζΩ(z)=1z+∑λ∈Ω∖{0}(1z−λ+1λ+zλ2).\zeta_\Omega(z)=\frac1z+\sum_{\lambda\in\Omega\setminus\{0\}} \left(\frac1{z-\lambda}+\frac1\lambda+\frac{z}{\lambda^2}\right).

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

ηΩ(ω)=ζΩ(ω1/2+ω)−ζΩ(ω1/2).\eta_\Omega(\omega)=\zeta_\Omega(\omega_1/2+\omega)-\zeta_\Omega(\omega_1/2).

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 ω≠0\omega\ne0 belong to Ω\Omega. Suppose u1,u2,ωu_1,u_2,\omega are linearly independent over Q\mathbb Q and

(Zu1+Zu2)∩Ω={0}.(\mathbb Z u_1+\mathbb Z u_2)\cap\Omega=\{0\}.

Define the indexed tuple

V=(g2,g3,ω,ηΩ(ω),u1,u2,℘(u1),ζΩ(u1),℘(u2),ζΩ(u2)).V=(g_2,g_3,\omega,\eta_\Omega(\omega),u_1,u_2, \wp(u_1),\zeta_\Omega(u_1),\wp(u_2),\zeta_\Omega(u_2)).

The proved conclusion is

∃i,j∈{0,…,9},i≠jand(Vi,Vj) is algebraically independent over Q.\exists i,j\in\{0,\ldots,9\},\quad i\ne j\quad\text{and}\quad (V_i,V_j)\text{ is algebraically independent over }\mathbb Q.

These are the hypotheses and conclusion of the paper's Theorem 1. No algebraicity assumption is imposed on g2g_2 or g3g_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∉Ωz,v,z+v\notin\Omega, write Δ=℘(v)−℘(z)\Delta=\wp(v)-\wp(z). They assert

2ΔζΩ(z+v)=2(ζΩ(z)+ζΩ(v))Δ+℘′(v)−℘′(z),2\Delta\zeta_\Omega(z+v) =2(\zeta_\Omega(z)+\zeta_\Omega(v))\Delta+\wp'(v)-\wp'(z),

and

4Δ2℘(z+v)=−4(℘(z)+℘(v))Δ2+(℘′(v)−℘′(z))2.4\Delta^2\wp(z+v) =-4(\wp(z)+\wp(v))\Delta^2+(\wp'(v)-\wp'(z))^2.

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

Nine completed milestones

MilestoneLinked result
Equation (5) — zeta addition identityProved
Equation (6) — elliptic addition identityProved
Lemma 6 — entire regularization and interpolation boundsProved
Lemma 8 — bounded auxiliary polynomial (formal-grid variant)Proved
Appendix A.2 — Weierstrass model realization (application bridge)Proved
Appendix A.2 / Lemma A.1 — subgroup degrees (application bridge)Proved
Proposition A.1 — zero estimate on the mission’s rank-one gridProved
Lemma 9 — bounded-order nonvanishing on the enlarged gridProved
Lemma 10 — nonzero small arithmetic elements (linear-degree variant)Proved

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 Z\mathbb Z-submodules of C\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 Q\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 u1,u2∉Ω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).
473 thms1 active userReviewed