Algebraic Geometry

Why rational torsion deserves a complete classification

An elliptic curve has rational solutions that can be added using a canonical group law. A torsion point is a rational solution that returns to the identity after a positive number of additions. These points form the finite part of the rational-point group and constrain which finite arithmetic configurations a curve can carry. Barry Mazur determined the possible groups uniformly over all elliptic curves defined over the rational numbers. The theorem is established mathematics; the remaining task is its complete formal proof, including the assertion that every permitted group occurs. The source is Theorem III.5.1 and its occurrence remark, printed page 156 of Modular curves and the Eisenstein ideal.

Curves, rational points, and finite additive order

A Weierstrass curve over the rational numbers is an equation

$$y^2+a_1xy+a_3y=x^3+a_2x^2+a_4x+a_6,$$

where all five coefficients are rational. Its discriminant measures singularity. The curves in this mission have nonzero discriminant, so they are elliptic curves. The group $E(\mathbb Q)$ consists of its rational points together with the distinguished point at infinity, which is the additive identity. The rational torsion subgroup is

$$E(\mathbb Q)_{\mathrm{tors}}=\{P\in E(\mathbb Q):\exists n\ge1,\ nP=0\}.$$

This subgroup is formed using the actual rational-point group; it is not a separately supplied finite group or a collection of coordinate certificates.

The symbol $\mathbb Z/n\mathbb Z$ denotes a cyclic group of order $n$, with its additive operation. A product of two such groups has componentwise addition. An additive group isomorphism is a bijection that preserves addition. Consequently, classifying a subgroup by an isomorphism identifies its complete group structure and its number of elements, rather than only the orders of selected points.

Formalization targets

For every elliptic curve $E/\mathbb Q$, the torsion subgroup must be finite and isomorphic to one of

$$\mathbb Z/n\mathbb Z\quad\text{for }n\in\{1,2,3,4,5,6,7,8,9,10,12\},$$

or

$$\mathbb Z/2\mathbb Z\times\mathbb Z/(2m)\mathbb Z\quad\text{for }m\in\{1,2,3,4\}.$$

Conversely, for every parameter in either displayed range, there must exist an elliptic curve over $\mathbb Q$ whose full rational torsion subgroup is isomorphic to that group. The curve may depend on the parameter. The goal combines unconditional finiteness, classification, and all fifteen occurrence cases. The cyclic case $n=1$ includes curves with trivial rational torsion. Occurrence requires equality of the entire torsion group up to isomorphism; constructing an embedding or a single point of the desired order does not meet that target.

The supporting point-order milestone is Corollary III.5.2, on the same source page: every rational point of positive finite order has order in the eleven-element cyclic list. Infinite-order points are outside that milestone's hypothesis. The four other milestone clauses separate finiteness, group classification, cyclic occurrence, and bicyclic occurrence so their contributions can be reviewed individually.

What the formal proof will provide

The final classification theorem will be available in the standard Lean vocabulary for rational elliptic curves, finite-order subgroups, cyclic groups, products, and additive equivalences. Its main downstream consumer is the canonical classification endpoint of the MazurTheorem repository. Occurrence supplies the converse needed for an exact list of possible groups. Together these results also give a torsion-cardinality bound of sixteen and uniformly exclude rational torsion configurations outside the list.

The existing repository contains substantial checked prerequisites and reductions. A prerequisite receives credit according to its actual hypotheses, conclusion, and connection to the acceptance theorem. This campaign does not treat the full classification as already formalized, and it does not treat locally checked source as a platform-verified contribution before transfer and verification. Existing proofs should be reused with their attribution and dependency graph intact. Open definitions and unproved mathematical comparisons must remain visible as obligations.

The remaining difficulty

Finite-abelian-group classification alone cannot establish which groups arise from an arbitrary rational elliptic curve. The crucial arithmetic exclusions require connecting concrete rational points with genuine arithmetic-geometric objects. A theorem about a supplied quotient or Jacobian does not construct that quotient or Jacobian; an interface that assumes a missing comparison leaves that comparison unproved. The foundational work includes represented modular curves, Jacobians and Picard functors, integral models, specialization, and the arithmetic needed to exclude prohibited point orders. These requirements reflect the mathematical source and the repository's current proof architecture.

The occurrence direction has a different verification obligation. Explicit rational points and order computations must be supplemented by a proof that the curve is nonsingular and that its entire rational torsion subgroup has precisely the claimed shape. Machine arithmetic and external tables can guide the selection of examples, but the published occurrence theorem must have a checked proof.

Formalization scope and contribution boundaries

Curves are Mathlib's WeierstrassCurve ℚ with IsElliptic; rational points are (E⁄ℚ).Point. Torsion is AddCommGroup.torsion, the cyclic groups are the additive groups of ZMod, and isomorphisms are additive equivalences. The target definition bundle repeats the repository's fifteen-group vocabulary in a campaign namespace. A checked compatibility bridge identifies its classification predicate with the repository's canonical predicate. This definition boundary exists solely to state platform obligations faithfully; its named consumers are the campaign goal and the repository's classification endpoint.

The goal has no supplied finiteness, rank, reduction, modularity, semistability, point-order classification, or group-classification hypothesis. Finiteness is an explicit conclusion. The numerical expression Set.ncard ≤ 16 is only a corollary: Set.ncard is zero on infinite sets, so that expression alone cannot certify this mission's completion. Checked proofs must have no placeholders, custom axioms, unchecked computation, or proof-strengthening options. The permitted foundational dependencies are propext, Quot.sound, and Classical.choice; open targets are displayed separately from their eventual proofs.

The repository's execution ledger remains the source of contributor assignment. Its selected foundations are the coherent-cohomology-to-Jacobian lane and the represented-modular-curve lane. Contracts marked paused remain paused unless the maintainers explicitly revise their assignment. Platform milestones describe mathematical completion obligations, not automatic authorization to claim every repository task. Contributors can close occurrence examples, reuse checked arithmetic reductions, and advance selected foundational packages with a concrete downstream consumer. Progress must track integrated obligations rather than code volume or the number of generated statements. Licenses, source commits, original authors, and upstream notices must accompany all transferred proofs.

Selected references

• Barry Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186. Part III, §5, Theorem (5.1), the following occurrence remark, and Corollary (5.2), printed p. 156. DOI; Numdam.
• Daniel S. Kubert, Universal bounds on the torsion of elliptic curves, Proceedings of the London Mathematical Society (3) 33 (1976), 193–237, especially Chapter IV's rational parametrizations, cited by Mazur's occurrence remark. DOI.
• Vasily Ilin and contributors, MazurTheorem, public Lean formalization. Repository; campaign source snapshot 54d43d8dda8a6fcf069cc02a815f850d762c5c0c. Existing uncommitted changes are excluded from source-snapshot claims.

Motivation

Mirror symmetry was discovered in string theory as a duality between families of Calabi–Yau manifolds, and it entered mathematics as a prediction: the generating function counting rational curves on one manifold equals a period integral of a mirror manifold. In his 1994 ICM address, Homological algebra of mirror symmetry (alg-geom/9411018), M. Kontsevich proposed that these numerical coincidences are shadows of an equivalence of categories: the symplectic geometry of $V$ should be encoded by Fukaya's $A_\infty$-category $F(V)$, whose objects are Lagrangian submanifolds and whose products count pseudo-holomorphic discs, and the complex geometry of the mirror $W$ by the derived category $D^b(\mathrm{Coh}\,W)$ of coherent sheaves. His Homological Mirror Conjecture asserts that the derived category built from $F(V)$ embeds as a full triangulated subcategory of $D^b(\mathrm{Coh}\,W)$.

Kontsevich states the conjecture "in slightly vague form", because Fukaya's construction was not, and still is not, available in the generality the statement needs. He therefore closes the paper with the one instance he can compute by hand, in the section Two-dimensional tori: a return: for the flat torus $\Sigma = \mathbb{R}^2/\mathbb{Z}^2$, the objects are closed geodesics with unitary local systems, the products $m_2$ are sums over triangles in the universal cover weighted by $\exp(-\text{area})$, and their structure constants are values of the classical theta-function. He predicts an equivalence with $D^b(\mathrm{Coh}\,E)$ for an elliptic curve $E$. This instance was proved by A. Polishchuk and E. Zaslow, Categorical mirror symmetry: the elliptic curve (math/9801119). Later instances include the four-torus (Abouzaid–Smith, arXiv:0903.3065) and Calabi–Yau hypersurfaces (Sheridan, arXiv:1111.0632). None of this has been formalized.

Setting

Fix a real number $\mathrm{area} > 0$, and let $\Sigma$ be the torus $\mathbb{R}^2/\mathbb{Z}^2$ carrying the translation-invariant symplectic form of total area $\mathrm{area}$; a region of Euclidean area $a$ in coordinates has symplectic area $\mathrm{area}\cdot a$.

A brane $b$ consists of: a primitive vector $v \in \mathbb{Z}^2$ and a point $c \in \mathbb{R}^2$, which together determine the closed geodesic $L_b = \{\,c + tv \bmod \mathbb{Z}^2\,\}$; a grading $\alpha \in \mathbb{R}$, a real lift of the direction angle normalized so that $(\cos \pi\alpha, \sin \pi\alpha)$ is parallel to $v$; and a real constant $\theta$ describing a flat unitary line bundle on $L_b$, whose parallel transport along a path of parameter length $s$ is $\exp(2\pi i\,\theta s)$. Two branes are transverse when $\det(v_1, v_2) \neq 0$; their geodesics then meet in the finite set $L_{b_1} \cap L_{b_2}$, which indexes a basis of the Floer space $\mathrm{Hom}(b_1, b_2)$. All of this space sits in a single degree, the Maslov index

$$\mu(b_1, b_2) \;=\; \lceil \alpha_2 - \alpha_1 \rceil .$$

For three pairwise transverse branes and intersection points $p \in L_1 \cap L_2$, $q \in L_2 \cap L_3$, $r \in L_1 \cap L_3$, a triangle is a triple of lifts $(P, Q, R) \in (\mathbb{R}^2)^3$ of $(p,q,r)$ with $Q - P$ parallel to $v_2$, $R - Q$ parallel to $v_3$, $P - R$ parallel to $v_1$, and positively oriented. Kontsevich's structure constant is

$$c(p,q,r) \;=\; \sum_{\text{triangles}} \exp\bigl(-\text{symplectic area}\bigr)\cdot \bigl(\text{holonomies along the three sides}\bigr),$$

the coefficient of $r$ in $m_2(p, q)$. On the complex side, $D^b_{\mathrm{coh}}(E)$ denotes the complexes of $\mathcal{O}_E$-modules with bounded, coherent cohomology.

Formalization targets

Goal — homological mirror symmetry for the two-torus

For every $\mathrm{area} > 0$ there exist a smooth proper curve $E$ over $\mathbb{C}$, an assignment $b \mapsto \Phi(b)$ of an object of $D^b_{\mathrm{coh}}(E)$ to each brane, and isomorphisms

$$\mathbb{C}^{\,L_{b_1} \cap L_{b_2}} \;\xrightarrow{\ \sim\ }\; \mathrm{Hom}\bigl(\Phi(b_1),\, \Phi(b_2)[\mu(b_1,b_2)]\bigr) \qquad (b_1 \pitchfork b_2),$$

with $\mathrm{Hom}(\Phi(b_1), \Phi(b_2)[d]) = 0$ for $d \neq \mu(b_1,b_2)$, carrying the products $c(p,q,r)$ to composition in $D^b_{\mathrm{coh}}(E)$ whenever $\mu(b_1,b_2) + \mu(b_2,b_3) = \mu(b_1,b_3)$.

Milestones

Existence of the Fukaya $A_\infty$-category of the torus; finiteness of $L_{b_1} \cap L_{b_2}$ with $|\det(v_1,v_2)|$ points; the Maslov relation $\mu(b_1,b_2) + \mu(b_2,b_1) = 1$; $m_1^2 = 0$ together with associativity of $m_2$ up to coboundary; the degeneration of an $A_\infty$-category with $m_{\geq 3} = 0$ to a differential graded category; the theta-function shape of the structure constants; and their associativity equation.

Significance

The conjecture reorganizes mirror symmetry: the numerical predictions compare two elements of an uncountable set of power series, whereas the homological statement compares two objects in a countable set of triangulated categories, and the numerical statements are meant to follow from it. The torus case is the smallest instance in which every ingredient — Lagrangian branes, Maslov grading, disc counts, theta functions, and coherent sheaves on an elliptic curve — is present and computable, so it is the natural first target.

What this mission adds beyond the literature is machine-checked mathematics where none exists. Mathlib currently has no symplectic manifolds, no Lagrangian Floer theory, no Fukaya categories, and no $A_\infty$-categories; it does have schemes, sheaves of modules, and derived categories of abelian categories. The mission supplies the missing $A_\infty$ layer and the torus model, and asks for the comparison theorem. The $A_\infty$ definitions, the derived category with coherent cohomology, and the theta-function estimates are reusable outside this mission.

Difficulty

The obvious route — "transport the Polishchuk–Zaslow proof" — stalls at the point where the two sides are compared. Establishing that the triangle sums converge and equal theta-function values is analysis that Mathlib supports; producing an elliptic curve as a scheme with prescribed parameter, computing $\mathrm{Ext}$-groups between the mirror sheaves, and matching all products simultaneously is not currently supported by any library. A second difficulty is bookkeeping: gradings, Maslov indices and shifts must line up, since the product of two morphisms is nonzero only when $\mu(b_1,b_2)+\mu(b_2,b_3) = \mu(b_1,b_3)$, and the same numerical condition controls which triples of branes bound triangles at all.

Formalization scope

Conventions committed to in Lean. An $A_\infty$-category is encoded as a single graded module $A$ with morphism components $\hom(X,Y)$ and products given by a map on lists, $m[f_1,\dots,f_n] = m_n(f_1 \otimes \cdots \otimes f_n)$ of degree $2-n$, with $m_0 = 0$, and Stasheff signs $(-1)^{r+st}$ in the bar-construction normalization; $m_2(f,g)$ is "$f$ then $g$". Triangles are normalized by requiring the first vertex to lie in $[0,1)^2$, which picks exactly one representative in each $\mathbb{Z}^2$-orbit; only positively oriented triangles are counted; sums are tsums, so convergence is part of the work. The hom-space isomorphisms in the goal are required to be additive, not a priori $\mathbb{C}$-linear, because the derived category of $\mathcal{O}_E$-modules is not equipped with a $\mathbb{C}$-linear structure in Mathlib; the required compatibility with the structure constants pins down the algebra anyway. The goal asks only for the existence of a smooth proper curve $E$ over $\mathbb{C}$; the paper's further prediction that $E$ has parameter $\exp(-\mathrm{area})$ is deliberately left out of the statement.

The goal is not trivially satisfiable: the intersection set of two transverse branes is nonempty, so the required isomorphisms force the corresponding $\mathrm{Hom}$-groups to be nonzero of the right size, in the right degree, with the prescribed products.

The general conjecture, for an arbitrary symplectic manifold with $c_1 = 0$, is not stated here, and deliberately so: without symplectic manifolds and Floer theory in Mathlib, any general statement would have to take the Fukaya category as an unconstrained parameter, which would make it either vacuous or false. Building that infrastructure — symplectic manifolds, graded Lagrangian branes, Floer cohomology, twisted complexes over an $A_\infty$-category and their triangulated structure — is the natural way to extend this mission, and such contributions are welcome.

Selected references

• M. Kontsevich, Homological algebra of mirror symmetry, Proceedings of the International Congress of Mathematicians (Zürich, 1994), alg-geom/9411018.
• A. Polishchuk and E. Zaslow, Categorical mirror symmetry: the elliptic curve, Adv. Theor. Math. Phys. 2 (1998), math/9801119.
• M. Abouzaid and I. Smith, Homological mirror symmetry for the 4-torus, Duke Math. J. 152 (2010), arXiv:0903.3065.
• N. Sheridan, Homological mirror symmetry for Calabi–Yau hypersurfaces in projective space, Invent. Math. 199 (2015), arXiv:1111.0632.

Motivation

Deciding whether a system of real polynomial equations, inequations and inequalities has a solution is the basic feasibility question behind nonconvex quadratic programming, polynomial optimization, robustness analysis in control, and combinatorial relaxations. Over the complex numbers, Hilbert's Nullstellensatz turns infeasibility into an algebraic identity whose bounded-degree instances are found by linear algebra. Over the reals this fails: $x^2+1=0$ has no real solution, yet $1$ is not in the ideal generated by $x^2+1$.

The real substitute is the Positivstellensatz of Stengle (Stengle 1974; see Bochnak–Coste–Roy, Real Algebraic Geometry, Theorem 4.4.2): a real polynomial system is infeasible exactly when an identity $f+g^2+h=0$ holds, with $f$ built from sums of squares and the inequality constraints, $g$ a product of the inequation polynomials and $h$ in the ideal of the equations. Parrilo (2003), building on his thesis (2000), observed that once the degrees are bounded, the search for such an identity is a semidefinite program (SDP), because a polynomial is a sum of squares exactly when it has a positive semidefinite Gram matrix. This yields a hierarchy of SDPs that is sound at every level and complete in the limit, and it is the origin of the sum-of-squares (SOS) method used throughout polynomial optimization.

Timeline:

• 1974: Stengle proves the Positivstellensatz for semialgebraic sets over real closed fields.
• 1995: Choi, Lam and Reznick analyze the Gram matrix method for sums of squares.
• 2000–2003: Parrilo (thesis; Math. Program. Ser. B 96) formulates bounded-degree Positivstellensatz refutations as SDPs (Theorem 5.1); Lasserre (2001) develops the dual moment approach independently.

Setting

Write $\mathbb R[x_1,\dots,x_n]$ for real polynomials in $n$ variables. Fix three finite, possibly empty, families: $f_1,\dots,f_s$ (inequalities), $g_1,\dots,g_t$ (inequations), $h_1,\dots,h_u$ (equations). They define the basic semialgebraic set

$$K=\{x\in\mathbb R^n \mid f_j(x)\ge 0,\ g_k(x)\ne 0,\ h_\ell(x)=0\ \text{for all } j,k,\ell\}.\qquad(4.4)$$

A cone of $\mathbb R[x_1,\dots,x_n]$ is a subset closed under addition and multiplication that contains every square $a^2$; $P(S)$ is the smallest cone containing $S$, and $P(\emptyset)$ is the set of sums of squares. $M$ is the multiplicative monoid generated by the $g_k$ (with the empty product $1$), and $I$ is the ideal generated by the $h_\ell$.

For a degree bound $D$, let $z$ be the vector of all monomials $x^\alpha$ of total degree at most $D$; it has $\binom{n+D}{D}$ entries. For a real matrix $Q$ indexed by these monomials, the Gram polynomial is $z^TQz=\sum_{\alpha,\beta}Q_{\alpha\beta}x^\alpha x^\beta$.

The degree-$d$ Positivstellensatz SDP $\mathrm{SDP}_d$: with $G=\sum_k\deg g_k$ and $N(d)=d(2G+1)$, find positive semidefinite matrices $Q_T$ over the monomials of degree at most $N(d)$, one for each $T\subseteq\{1,\dots,s\}$, and polynomials $q_\ell$ of degree at most $2N(d)$, such that

$$\sum_{T}(z^TQ_Tz)\prod_{j\in T}f_j+\Big(\prod_{k=1}^t g_k^{2d}\Big)^2+\sum_{\ell=1}^u q_\ell h_\ell=0 .$$

Its unknowns are finitely many real numbers, the constraint is linear in them, and the matrices are constrained to be positive semidefinite.

Formalization targets

Goal: Theorem 5.1

$$\big(\forall d,\ \mathrm{SDP}_d\ \text{feasible}\Rightarrow K=\emptyset\big)\quad\text{and}\quad\big(K=\emptyset\Rightarrow\exists d_0\ \forall d\ge d_0,\ \mathrm{SDP}_d\ \text{feasible}\big).$$

The first half says every feasible point is a refutation; the second says the hierarchy is complete once the degree bound is large enough. No bound on $d_0$ is asserted, matching the paper.

Milestones

• Theorem 4.6, $2\Rightarrow1$: an identity $f+g^2+h=0$ with $f\in P$, $g\in M$, $h\in I$ forces $K=\emptyset$.
• A positive semidefinite Gram matrix gives a sum of squares (§3.2).
• Theorem 4.6, $1\Rightarrow2$ (Stengle's Positivstellensatz): $K=\emptyset$ forces such an identity.
• $P(\emptyset)$ is the set of sums of squares and the smallest cone; the finite-generator form $P(S)=\{p+\sum_i q_ib_i\}$; the squarefree form $\sum_T p_T\prod_{j\in T}f_j$ of the cone used in the proof of Theorem 5.1.
• A sum of squares of degree at most $2d$ has a positive semidefinite Gram matrix over the monomials of degree at most $d$; Theorem 3.3 combining both directions with the size $\binom{n+d}{d}$; the count $\binom{n+d}{d}$ of the monomial vector.

Significance

Theorem 5.1 is the statement that makes Positivstellensatz certificates computable: it converts an existence theorem of real algebraic geometry into a sequence of convex feasibility problems, each solvable by interior-point methods, and any solution is an exact proof of infeasibility. Lower bounds in polynomial optimization (Example 5.4), the copositivity tests of §7.5, SOS relaxations for MAX-CUT and stable sets, and Lyapunov-function searches in control are all instances of this scheme.

The paper proves only the soundness direction of the Positivstellensatz and cites the converse. A complete formal development therefore contains the first machine-checked statement chain from Stengle's theorem to the SDP hierarchy. To the best of current searches, neither Mathlib nor Prove2Me contains the real Positivstellensatz, the Gram matrix characterization of sums of squares, or the monomial count; Mathlib has sums of squares in rings (IsSumSq), positive semidefinite matrices, and the complex Nullstellensatz.

Difficulty

The soundness half is elementary. Completeness rests on Stengle's Positivstellensatz, whose standard proofs pass through real closed fields, orderings of rings and the Tarski–Seidenberg transfer principle, none of which is available in Mathlib in usable form. A tempting shortcut, proving completeness by reasoning only about $\mathbb R$-points, does not work: the certificate must be an algebraic identity, and points cannot produce it.

A second, smaller difficulty is degree bookkeeping. Each level of the hierarchy has a fixed shape (the exponent of the $g_k$ and the degree of every multiplier are tied to $d$), while a certificate supplied by the Positivstellensatz has arbitrary degrees and exponents. A Gram representation also needs a degree bound on every square in a sum of squares, not only on the sum.

Formalization scope

• Polynomials are MvPolynomial (Fin n) ℝ; $n,s,t,u$ are arbitrary natural numbers, including $0$; the families are indexed by Fin s, Fin t, Fin u. The set (4.4) lives in $\mathbb R^n$ = Fin n → ℝ.
• $P(S)$ is the smallest set closed under $+$, $\cdot$ and containing all squares (Definition 4.5), an inductive predicate. Mathlib's RingPreordering is not used: it excludes $-1$, which an infeasible system's cone typically contains.
• Sums of squares are IsSumSq; positive semidefiniteness is Matrix.PosSemidef (symmetric, which is the paper's $Q\in\mathcal S^n$); $M$ is Submonoid.closure, $I$ is Ideal.span.
• The meta-claim "the search … can be done using semidefinite programming" is the definition of $\mathrm{SDP}_d$: finitely many PSD Gram matrices indexed by a finite type of monomials, and ideal multipliers of bounded total degree. The degree choices ($m=d$ in $g=\prod g_k^{2m}$; multiplier degree $d_2=2d(2G+1)$) fill the freedom the proof leaves and satisfy its printed bounds $d_2\ge d$, $d_2\ge\deg g$. "Large enough" is $\exists d_0\,\forall d\ge d_0$.
• A formalization without the degree bounds or with an infinite index type would make $\mathrm{SDP}_d$ equivalent to Theorem 4.6 item 2 and is ruled out; so is a goal stated for a fixed $n$, for empty families only, or with soundness only at large $d$.
• Needed infrastructure: Stengle's Positivstellensatz over $\mathbb R$ (real closed field theory or a direct proof), the Gram matrix correspondence, and degree lemmas for sums of squares. The Positivstellensatz and the Gram correspondence are reusable far beyond this mission; contributions toward either are welcome.

Selected references

• P. A. Parrilo, Semidefinite programming relaxations for semialgebraic problems, Math. Program. Ser. B 96 (2003) 293–320. https://doi.org/10.1007/s10107-003-0387-5
• G. Stengle, A Nullstellensatz and a Positivstellensatz in semialgebraic geometry, Math. Ann. 207 (1974) 87–97. https://doi.org/10.1007/BF01362149
• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998, Theorem 4.4.2. https://doi.org/10.1007/978-3-662-03718-8
• M. D. Choi, T. Y. Lam, B. Reznick, Sums of squares of real polynomials, Proc. Sympos. Pure Math. 58 (1995) 103–126. https://doi.org/10.1090/pspum/058.2/1327293
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11 (2001) 796–817. https://doi.org/10.1137/S1052623400366802

Motivation

A classical way to recognize an algebraic function is through the arithmetic of its Taylor coefficients. Eisenstein's theorem (1852) says that if a power series $f\in\mathbb{Q}[[z]]$ is algebraic over $\mathbb{Q}[z]$, only finitely many primes occur in the denominators of its coefficients. The converse fails in general: many transcendental power series have integer coefficients. Lam and Litt (arXiv:2501.13175) conjecture that the converse does hold for power series that solve an algebraic differential equation at a non-singular point, and that even a weak control on denominators — primes $p$ may appear, but only after roughly $\omega(p)\gg p$ coefficients — already forces algebraicity.

For linear differential equations, the conjecture is a strengthening of the Grothendieck–Katz $p$-curvature conjecture, one of the central open problems about algebraic solutions of linear differential equations (arXiv:2501.13175). The bounded-denominator form is Problem 1 on Litt's list of open problems (problemsilike.com/1).

Timeline.

• 1852 — Eisenstein: algebraic power series over $\mathbb{Q}$ have bounded denominators (implication (1)⇒(2) below).
• 1970s — Grothendieck and Katz: the $p$-curvature conjecture for linear differential equations.
• 2025 — Lam and Litt formulate the conjecture for (possibly non-linear) algebraic differential equations and prove it for many equations and initial conditions of algebro-geometric interest, including Picard–Fuchs equations at initial conditions corresponding to cycle classes, and isomonodromy equations such as Painlevé VI and the Schlesinger system at initial conditions corresponding to Picard–Fuchs equations (arXiv:2501.13175).

Setting

Let $f=\sum_{k\ge0}a_kz^k\in\mathbb{Q}[[z]]$ be a formal power series with rational coefficients and write $f^{(i)}$ for its $i$-th formal derivative. Let $g\in\mathbb{Q}(z,y_0,\dots,y_{n-1})$ be a rational function in $n+1$ variables. The series $f$ solves the algebraic ODE defined by $g$ if

$$f^{(n)}(z)=g\bigl(z,f(z),f'(z),\dots,f^{(n-1)}(z)\bigr)$$

and $g$ is defined at $\bigl(0,f(0),\dots,f^{(n-1)}(0)\bigr)$. Concretely, $g=p/q$ for polynomials $p,q$ with $q\bigl(0,f(0),\dots,f^{(n-1)}(0)\bigr)\neq0$ and $f^{(n)}\cdot q(z,f,\dots,f^{(n-1)})=p(z,f,\dots,f^{(n-1)})$.

For $N\in\mathbb{N}$, $\mathbb{Z}[1/N]\subseteq\mathbb{Q}$ is the subring generated by $1/N$. For a function $\omega$ from the primes to $\mathbb{Z}$, the coefficients of $f$ are $\omega$-integral if for every prime $p$ the numbers $a_0,\dots,a_{\omega(p)}$ lie in $\mathbb{Z}_{(p)}$ (denominators prime to $p$); $\omega$ is superlinear if $\omega(p)/p\to\infty$.

Formalization targets

Goal: the Lam–Litt conjecture

For $f$ solving an algebraic ODE as above, the following are equivalent:

$$\text{(1) } f \text{ is algebraic over } \mathbb{Q}[z];\qquad \text{(2) } \exists N,\ \forall k,\ a_k\in\mathbb{Z}[1/N];\qquad \text{(3) } \exists\,\omega \text{ superlinear with } (a_k) \ \omega\text{-integral}.$$

Milestones

• (1)⇒(2), Eisenstein's theorem (no ODE hypothesis needed).
• (2)⇒(3), elementary (no ODE hypothesis needed).
• (3)⇒(2), open.
• (2)⇒(1), open; Litt's Problem 1.

Together the four milestones imply the goal; the last two are the open content of the conjecture.

Significance

A proof would give an arithmetic criterion for algebraicity of solutions of arbitrary algebraic differential equations, and, for linear equations, would imply the Grothendieck–Katz $p$-curvature conjecture (arXiv:2501.13175). Lam and Litt draw algebro-geometric consequences from the cases they prove.

For formalization: the conjecture is open, so the goal and the two open milestones are research targets. Eisenstein's theorem is a classical result; formalizing it is concrete, self-contained work. The implication (2)⇒(3) is elementary. The cases proved by Lam and Litt are candidates for further milestones.

Difficulty

Integrality of coefficients alone does not detect algebraicity: there are transcendental power series with integer coefficients that satisfy linear differential equations, such as $\sum_k\binom{2k}{k}^2z^k$. Its equation is singular at $z=0$, which the non-singularity hypothesis on $g$ excludes; the conjecture asserts that at non-singular points such examples cannot occur. Even for linear equations the statement contains the Grothendieck–Katz conjecture, which is open in general.

Formalization scope

• Power series are PowerSeries ℚ with the formal derivative; rational functions are the fraction field of MvPolynomial (Fin (n + 1)) ℚ, where variable 0 is $z$ and variable i + 1 is $f^{(i)}$.
• The ODE hypothesis is existential: some representation $g=p/q$ with $q$ nonzero at the initial point and $f^{(n)}q(\dots)=p(\dots)$ as power series. This non-singularity requirement is essential and must not be dropped.
• Algebraicity is IsAlgebraic (Polynomial ℚ) f, i.e. over $\mathbb{Q}[z]$ (equivalently over $\mathbb{Q}(z)$).
• $\mathbb{Z}[1/N]$ is the subalgebra of $\mathbb{Q}$ generated by $1/N$; since $1/0=0$ in Lean, $N=0$ gives $\mathbb{Z}$.
• $\omega$ takes values in $\mathbb{Z}$; negative values impose no condition at that prime. Superlinearity is the limit $\omega(p)/p\to\infty$ along the primes.
• The goal is a List.TFAE of the three conditions.

Useful infrastructure: formal derivatives and substitution for power series, algebraic power series and their coefficient arithmetic (Eisenstein), and $p$-adic valuations of coefficients. Formalizations of Eisenstein's theorem and of the special cases proved by Lam and Litt are welcome.

Selected references

• Y. H. J. Lam, D. Litt, Algebraicity and integrality of solutions to differential equations, arXiv preprint, 2025. https://arxiv.org/abs/2501.13175
• D. Litt, Problem 1, problems list. https://www.problemsilike.com/1
• G. Eisenstein, Über eine allgemeine Eigenschaft der Reihen-Entwicklungen aller algebraischen Funktionen, Bericht der Königl. Preuss. Akademie der Wissenschaften zu Berlin, 1852.
• Formal Conjectures project, FormalConjectures/LittProblems/1.lean. https://github.com/google-deepmind/formal-conjectures

Motivation

A $2n$-dimensional complex abelian variety $A$ is of Weil type for an imaginary quadratic field $K=\mathbb{Q}(\sqrt{-d})$ if $K$ acts on $A$ by rational endomorphisms in such a way that each of the two eigenspaces of $\sqrt{-d}$ on $H^1(A,\mathbb{C})$ meets $H^{1,0}(A)$ in an $n$-dimensional subspace. A. Weil observed that such $A$ carry a two-dimensional space of rational $(n,n)$-classes, the Hodge–Weil classes, that are in general not generated by divisor classes. Whether they are algebraic is one of the main test cases of the Hodge conjecture; by work of Schoen, Moonen–Zarhin and others, algebraicity for abelian fourfolds of Weil type implies the Hodge conjecture for all abelian fourfolds.

E. Markman (arXiv:2502.03415) proves this algebraicity by a new construction. Its starting point, developed in §§1.2 and 2 of the paper, is linear algebra: the even cohomology $H^{\mathrm{ev}}(X)$ of an abelian $n$-fold $X$ is a half-spin representation of $\mathrm{Spin}(V)$, where $V=H^1(X,\mathbb{Z})\oplus H^1(\hat X,\mathbb{Z})$, and a rational plane $P\subset H^{\mathrm{ev}}(X,\mathbb{Q})$ meeting the variety of pure spinors in two conjugate $K$-points (a $K$-secant) equips $X\times\hat X$ with the structure of an abelian variety of Weil type. This mission formalizes that construction and its explicit example in §2.4.

Timeline (as summarized in §1.1 of the source).

• Weil introduces abelian varieties of Weil type and their exceptional Hodge classes.
• Schoen proves algebraicity for fourfolds with $K=\mathbb{Q}(\sqrt{-3})$ (and for sixfolds with $K=\mathbb{Q}(\sqrt{-3})$ and trivial discriminant), and for fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$; van Geemen gives another proof of the latter.
• Koike treats sixfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$; Markman treats fourfolds with arbitrary $K$ and discriminant $1$.
• 2025: Markman proves algebraicity for sixfolds of discriminant $-1$ and every $K$, hence for all abelian fourfolds of Weil type.

Setting

Let $X$ be a complex torus of dimension $n$. Fix a basis of $H^1(X,\mathbb{Z})$, so that $H^1(X,\mathbb{C})=\mathbb{C}^{2n}$, and write $H^1(\hat X)\cong H^1(X)^*$ in dual coordinates. The complex structure of $X$ is a real matrix $J$ with $J^2=-1$ acting on $H^1(X,\mathbb{R})$; its $i$-eigenspace is $H^{1,0}(X)$. A number $z\in\mathbb{C}$ acts on $H^1(X,\mathbb{C})$ by $\operatorname{Re}z+\operatorname{Im}z\,J$ and on $H^k(X,\mathbb{C})=\wedge^kH^1(X,\mathbb{C})$ multiplicatively; a class of type $(p,q)$ is multiplied by $z^p\bar z^q$. The Hodge ring is $\bigoplus_pH^{p,p}(X,\mathbb{Q})$.

• $V_{\mathbb{C}}=H^1(X,\mathbb{C})\oplus H^1(\hat X,\mathbb{C})$ carries the pairing $((w_1,t_1),(w_2,t_2))_V=t_1(w_2)+t_2(w_1)$ and the complex structure $I=J\oplus(-J^{\mathsf T})$ of $X\times\hat X$; $V^{1,0},V^{0,1}$ are the $\pm i$-eigenspaces of $I$.
• $S_{\mathbb{C}}=H^*(X,\mathbb{C})=\wedge^*H^1(X,\mathbb{C})$ is the spin representation: $v=(w,t)$ acts by $m_v(s)=w\wedge s+D_t(s)$, with $D_t$ the contraction. A nonzero $s\in S^+_{\mathbb{C}}=H^{\mathrm{ev}}(X,\mathbb{C})$ is an even pure spinor if its annihilator $W_s=\{v:m_v(s)=0\}$ has dimension $2n$ (it is then maximal isotropic).
• For $d>0$ put $\sqrt{-d}=i\sqrt d$ and $K=\mathbb{Q}(\sqrt{-d})$. Given rational $a,b\in S^+$ with $\lambda_{1,2}=a\pm\sqrt{-d}\,b$ even pure spinors, the line $\mathbb{P}(P)$, $P=\operatorname{span}_{\mathbb{Q}}(a,b)$, is a $K$-secant to the spinor variety, with $W_1=W_{\lambda_1}$, $W_2=W_{\lambda_2}$. When $W_1\cap W_2=0$, the endomorphism $f=\eta_{\sqrt{-d}}$ acting by $\pm\sqrt{-d}$ on $W_{1,2}$ is rational (2.2.4), (2.4.1); $\Xi_P(x,y)=(f(x),y)_V$ and $g_P(x,y)=\Xi_P(I(x),y)$.
• For an ample class $\Theta\in H^{1,1}(X,\mathbb{Z})$ put $u=\sqrt{-d}\,\Theta$ and $P=\operatorname{span}\{\operatorname{Re}\exp(u),\operatorname{Im}\exp(u)/\sqrt d\}$ (2.4.5).

Formalization targets

Goal (Proposition 2.4.4, with (2.4.6) and Lemma 2.2.6)

For a complex torus $X$ of dimension $n\ge2$ with ample $\Theta$, and a positive integer $d$: $\exp(\pm\sqrt{-d}\,\Theta)$ are even pure spinors with $W_1\cap W_2=0$, and there is a rational $f$ acting by $\pm\sqrt{-d}$ on $W_{1,2}$ with

$$f^2=-d,\quad (fx,fy)_V=d\,(x,y)_V,\quad fI=If,\quad \dim(W_i\cap V^{1,0})=n,\quad g_P(x,x)<0\ \ (0\neq x\in V_{\mathbb{R}}).$$

That is, $(X\times\hat X,\eta,\Xi_P)$ is a polarized abelian variety of Weil type.

Milestones

Equation (2.4.6) (the annihilator of $\exp(u)$), Equation (2.4.5) (the plane lies in the Hodge ring), Lemma 2.2.6 (Weil's condition), the rational similarity $f$ of (2.2.4)/(2.4.1), the commutation $fI=If$ (§2.4, p. 20), and Lemma 2.4.2 (the formula for $g_P$).

Significance

The result. The construction supplies, for every imaginary quadratic field $K$ and every polarized abelian $n$-fold, a polarized abelian variety of Weil type $X\times\hat X$, together with a description of its Weil structure in spin-representation terms. The rest of the paper deforms this structure ($\mathrm{Spin}(V)_P$ plays the role of the special Mumford–Tate group) and uses Orlov's derived equivalence to obtain the Hodge–Weil classes from sheaves; the final application is the Hodge conjecture for abelian fourfolds.

Formalizing it. The results of this mission are proved in the paper; none of them has a machine-checked proof. The mission produces a reusable Lean model of the spin representation $H^*(X)$ of $V=H^1(X)\oplus H^1(\hat X)$, of pure spinors and their annihilators, and of Hodge types on $\wedge^*H^1$, all built on Mathlib's exterior and Clifford algebras.

Difficulty

The algebra in the explicit example is short, but the general milestones rest on facts about pure spinors (their annihilators are maximal isotropic; a conjugate pair with $W_1\cap W_2=0$ splits $V_K$; rationality of $f$ by Galois descent) and on Lemma 2.2.6, whose proof in the source uses Chevalley's isomorphism $S\otimes S\cong C(V)$ as a morphism of Hodge structures. A coordinate computation settles the example but not the general statements. Sign conventions (the choice of $\sqrt{-d}$, the complex structure on $H^1(\hat X)$, and the sign of ampleness) all enter the final negativity claim.

Formalization scope

• Everything is linear algebra over $\mathbb{C}$, with the rational and integral structures given by the coordinate basis; $X$ is a complex torus carrying the class $\Theta$.
• $H^*(X,\mathbb{C})$ is ExteriorAlgebra ℂ (Fin (2n) → ℂ); contraction is Mathlib's CliffordAlgebra.contractLeft; $\exp$ is the truncated exponential $\sum_{k\le2n}s^k/k!$.
• The complex structure of $V_{\mathbb{R}}$ is $I=J\oplus(-J^{\mathsf T})$, the extension of $J$ that is an isometry of $(\cdot,\cdot)_V$ (footnote 8 of the source).
• Ampleness sign. Ampleness is encoded as it is used in the proof of Proposition 2.4.4: $\Theta\in H^{1,1}(X,\mathbb{Z})$ and $\Theta(a\wedge I(a))>0$ for nonzero $a\in H^1(\hat X,\mathbb{R})$, with $I=-J^{\mathsf T}$ on $H^1(\hat X,\mathbb{R})$. With the opposite sign the last clause of the goal would become positive definiteness.
• $W_1\cap W_2=0$ is a hypothesis of the general milestones; in the source it is deduced from the non-isotropy of $P$ via Lemma 2.2.1.
• Not included: the spin group, the stabilizer $\mathrm{Spin}(V)_P$, the centralizer statement of Lemma 2.2.4 and the discriminant computation of Lemma 3.1.3. Contributions adding these are welcome.

Selected references

• E. Markman, Cycles on abelian 2n-folds of Weil type from secant sheaves on abelian n-folds, arXiv:2502.03415v2, 2025. https://arxiv.org/abs/2502.03415
• C. Chevalley, The algebraic theory of spinors, Columbia University Press, 1954.
• B. van Geemen, An introduction to the Hodge conjecture for abelian varieties, in: Algebraic Cycles and Hodge Theory, LNM 1594, Springer, 1994. https://doi.org/10.1007/BFb0074000
• P. Deligne, The Hodge conjecture, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/hodge.pdf

Motivation

For a field $F$, two invariants built from very different data turn out to carry the same mod-2 information. One is Milnor K-theory $K^M_n(F)$, defined by generators and relations from the multiplicative group $F^\times$ alone. The other is Galois cohomology $H^n(F,\mathbb{Z}/2)$, the continuous cohomology of the absolute Galois group of $F$. In 1970 Milnor considered a natural map $K^M_n(F)/2 \to H^n(F,\mathbb{Z}/2)$ in all degrees, verified that it is an isomorphism for several classes of fields, and remarked that he knew of no field where it fails (Milnor 1970). The statement that it is always an isomorphism when $\operatorname{char} F \neq 2$ became known as the Milnor conjecture. Its companion conjecture on quadratic forms was later deduced from it (Orlov–Vishik–Voevodsky 2007). Together they identify the graded Witt ring of quadratic forms, Galois cohomology mod 2, and $K^M_*(F)/2$.

Timeline. The attributions below follow the introduction of Voevodsky 2003.

• 1970: Milnor considers the map $K^M_n(F)/2 \to H^n(F,\mathbb{Z}/2)$ in all degrees and gives classes of fields where it is an isomorphism (Milnor 1970).
• Bass–Tate (published 1973): the Kummer classes satisfy the Steinberg relation, so the Kummer map extends to a ring homomorphism on $K^M_*(F)$ (Bass–Tate 1973).
• Degrees 0 and 1: the map is an isomorphism, by Kummer theory and Hilbert's Theorem 90.
• 1981: Merkurjev proves degree 2 with $2$ as the coefficient prime.
• 1982: Merkurjev and Suslin extend degree 2 to every prime $\ell$ (Merkurjev–Suslin 1982).
• Degree 3, $\ell = 2$: proved by Merkurjev–Suslin and, independently, by Rost.
• 2003: Voevodsky proves all degrees, in every characteristic $\neq 2$ (Voevodsky 2003, Cor. 7.5), using the motivic Steenrod operations constructed in Voevodsky 2003b. This work was cited for his 2002 Fields Medal.
• 2011: the analogue for odd primes, the Bloch–Kato conjecture, is proved (Voevodsky 2011); a book-length account is Haesemeyer–Weibel 2019.

Setting

Let $F$ be a field with $2 \neq 0$ in $F$.

Milnor K-theory. For $n \ge 0$, $K^M_n(F)$ is the quotient of the $n$-fold tensor power $(F^\times)^{\otimes n}$, taken over $\mathbb{Z}$ with $F^\times$ written additively, by the subgroup generated by the pure tensors $a_1\otimes\cdots\otimes a_n$ in which some adjacent pair satisfies $a_i + a_{i+1} = 1$. This is the degree-$n$ part of $T(F^\times)/I$, where $I$ is the two-sided ideal generated by $a\otimes(1-a)$. The class of $a_1\otimes\cdots\otimes a_n$ is the symbol $\{a_1,\dots,a_n\}$. In particular $K^M_0(F) = \mathbb{Z}$ and $K^M_1(F) = F^\times$. In Lean these are MilnorK F n and symbol a for a : Fin n → Fˣ.

Galois cohomology. Let $F^{\mathrm{sep}}$ be a separable closure and $G_F = \operatorname{Gal}(F^{\mathrm{sep}}/F)$ the absolute Galois group, a profinite group under the Krull topology. $H^n(F,\mathbb{Z}/2)$ is the continuous cohomology $H^n_{\mathrm{cts}}(G_F,\mathbb{Z}/2)$ with trivial action, computed from $G_F$-invariant continuous homogeneous cochains. In Lean this is H F n, Mathlib's continuousCohomology n of the trivial representation.

The Galois symbol. For $a \in F^\times$ fix $\sqrt a \in F^{\mathrm{sep}}$. The Kummer character $\chi_a : G_F \to \mathbb{Z}/2$ is $\chi_a(\sigma) = 0$ if $\sigma(\sqrt a) = \sqrt a$ and $1$ otherwise. It is a continuous homomorphism representing the Kummer class $\delta a \in H^1$. The Galois symbol of $(a_1,\dots,a_n)$ is the class of the homogeneous cocycle

$$(x_0,\dots,x_n)\ \longmapsto\ \prod_{j=1}^{n}\bigl(\chi_{a_j}(x_j)-\chi_{a_j}(x_{j-1})\bigr),$$

the homogeneous form of $(\sigma_1,\dots,\sigma_n) \mapsto \chi_{a_1}(\sigma_1)\cdots\chi_{a_n}(\sigma_n)$, i.e. the cup product $\delta a_1\cup\cdots\cup\delta a_n$. In Lean this is galoisSymbol a.

Formalization targets

Goal: the Milnor conjecture (Voevodsky 2003, Corollary 7.5)

For every field $F$ with $\operatorname{char} F \neq 2$ and every $n \ge 0$ there is a homomorphism

$$\varphi : K^M_n(F) \to H^n(F,\mathbb{Z}/2),\qquad \varphi\{a_1,\dots,a_n\} = \delta a_1\cup\cdots\cup\delta a_n,$$

which is surjective and whose kernel is exactly $2\,K^M_n(F)$.

Since symbols generate $K^M_n(F)$, such a $\varphi$ is unique; it is the norm residue homomorphism. The statement is therefore equivalent to $K^M_n(F)/2 \cong H^n(F,\mathbb{Z}/2)$ via the norm residue map. Its existence, i.e. the fact that the Steinberg relations map to zero, is part of the claim.

Significance

The result itself. The theorem gives a presentation of mod-2 Galois cohomology by generators and relations: every class is a sum of cup products of degree-one classes, and every relation among such products comes from Steinberg relations and multiples of 2. With Orlov–Vishik–Voevodsky 2007 it yields Milnor's conjecture on quadratic forms, which classifies quadratic forms up to Witt equivalence by their Galois-cohomological invariants.

Formalizing it. The theorem is proved but not formalized. At the time of writing, Mathlib has neither Milnor K-theory nor cup products in group or continuous cohomology, and has Hilbert 90 only for finite Galois extensions. This mission's definitions provide a sorry-free Galois symbol in Mathlib's continuous cohomology, which already makes the degree 0 and degree 1 cases (Kummer theory) meaningful targets. A complete development would formalize the IHES proof, including motivic cohomology with $\mathbb{Z}/2$ coefficients and the motivic Steenrod algebra. No part of that is currently available in Lean. Related existing work: on this platform, a graded cup product (groupCohomology.exists_isGradedCupProduct) and a Kummer theory and Hilbert 90 for level-constant cocycles have been formalized on top of Mathlib's discrete groupCohomology. The cup product is for discrete groups, and the Kummer and Hilbert 90 results use finite-level hypotheses in place of continuity, so none of them transfers directly to continuousCohomology.

Difficulty

Degrees 0 and 1 follow from Kummer theory and Hilbert 90. Degree 2 is Merkurjev's theorem, whose proof goes through the K-theory of Severi–Brauer varieties. No argument internal to Galois cohomology or K-theory of fields is known in higher degrees. The known proof reformulates the statement as a vanishing theorem for motivic cohomology of fields, the "Hilbert 90" property for weight $n$. It then argues by induction on $n$ through geometry over $F$: splitting varieties of symbols (Pfister quadrics), their motives, and cohomology operations on motivic cohomology. Each of these is a substantial theory, none of it exists in Mathlib, and the induction passes through statements about arbitrary smooth varieties, not only fields.

Formalization scope

Scope. The target is the Milnor conjecture, i.e. the prime $2$ with coefficients $\mathbb{Z}/2 \cong \mu_2$. The Bloch–Kato conjecture for odd primes is out of scope.

Conventions.

• The field is F : Type, universe 0. Mathlib's continuousCohomology requires the coefficient module to live in the universe of the group. For $F$ in a higher universe this forces ULift (ZMod 2), for which the needed Module and ContinuousSMul instances are not available as global instances. Universe polymorphism is not part of this mission. It does not follow by plain transport, since a field in a higher universe need not be isomorphic to any field in Type; one route is a limit argument, using that both sides commute with directed unions of fields and that every field is the directed union of its countable subfields, each isomorphic to a field in Type.
• The hypothesis $\operatorname{char} F \neq 2$ is [NeZero (2 : F)].
• $H^n$ is Mathlib's continuousCohomology, built from homogeneous cochains, with $\mathbb{Z}/2$ as a trivial representation of $G_F$ with the Krull topology.
• $K^M_n(F)$ is defined one degree at a time, not as a graded ring.
• "Kernel $= 2K^M_n$" means $\varphi(x)=0 \iff \exists y,\ x = 2y$.

Ruling out trivializations. The Galois symbol is not a free parameter. It is a fixed, sorry-free definition, and the existence of $\varphi$ with the prescribed values on symbols is part of the goal. Neither can be chosen to make the statement vacuous.

Route. Reductions should follow Voevodsky 2003 together with Voevodsky 2003b. That route avoids resolution of singularities and works in every characteristic $\neq 2$. The following rely on resolution of singularities (or on characteristic-0 reductions) and should not be used as inputs:

• Mazza–Voevodsky–Weibel (MVW 2006), results 16.24, 16.25 and 20.1, and the cdh-topology and compactly-supported-motive material;
• the original Suslin–Voevodsky paper relating Bloch–Kato to Beilinson–Lichtenbaum (Suslin–Voevodsky 2000); use Haesemeyer–Weibel 2019, Chapter 2, instead;
• Haesemeyer–Weibel Part II, and their reduction to characteristic 0 (Lemma 1.3);
• Voevodsky's 1995–96 preprints on the Milnor conjecture.

Infrastructure needed and reusable. A complete development needs:

• the ring structure on $K^M_*(F)$ (cf. Carlier's KMilnorWitt for Milnor–Witt K-theory);
• cup products in continuous cohomology;
• Hilbert 90 for profinite Galois groups;
• Galois cohomology as étale cohomology of $\operatorname{Spec} F$;
• the Nisnevich topology;
• presheaves with transfers, motivic complexes and motivic cohomology;
• motivic Steenrod operations;
• motives of Pfister quadrics.

Most of this is reusable well beyond the mission. The homogeneous-cochain construction in the definition files, which turns an invariant continuous cocycle $G^{n+1}\to M$ into a class in Mathlib's continuousCohomology, applies to any locally compact group with trivial coefficients. Contributions of any of these components, and of the degree 0 and 1 cases, are welcome.

Selected references

• V. Voevodsky, Motivic cohomology with $\mathbb{Z}/2$-coefficients, Publ. Math. IHÉS 98 (2003), 59–104. https://doi.org/10.1007/s10240-003-0010-6
• V. Voevodsky, Reduced power operations in motivic cohomology, Publ. Math. IHÉS 98 (2003), 1–57. https://doi.org/10.1007/s10240-003-0009-z
• J. Milnor, Algebraic K-theory and quadratic forms, Invent. Math. 9 (1970), 318–344. https://doi.org/10.1007/BF01425486
• H. Bass, J. Tate, The Milnor ring of a global field, in Algebraic K-theory II, Lecture Notes in Math. 342, Springer, 1973. https://doi.org/10.1007/BFb0073733
• A. S. Merkurjev, A. A. Suslin, K-cohomology of Severi–Brauer varieties and the norm residue homomorphism, Math. USSR Izv. 21 (1983). https://doi.org/10.1070/IM1983v021n02ABEH001793
• D. Orlov, A. Vishik, V. Voevodsky, An exact sequence for $K^M_*/2$ with applications to quadratic forms, Ann. of Math. 165 (2007), 1–13. https://doi.org/10.4007/annals.2007.165.1
• V. Voevodsky, On motivic cohomology with $\mathbb{Z}/l$-coefficients, Ann. of Math. 174 (2011), 401–438. https://doi.org/10.4007/annals.2011.174.1.11
• C. Haesemeyer, C. Weibel, The Norm Residue Theorem in Motivic Cohomology, Annals of Math. Studies 200, Princeton, 2019. https://doi.org/10.1515/9780691189635
• C. Mazza, V. Voevodsky, C. Weibel, Lecture Notes on Motivic Cohomology, Clay Math. Monographs 2, AMS, 2006. https://www.claymath.org/wp-content/uploads/2022/03/Motivic-Cohomology.pdf
• A. Suslin, V. Voevodsky, Bloch–Kato conjecture and motivic cohomology with finite coefficients, in The Arithmetic and Geometry of Algebraic Cycles, NATO Sci. Ser. C 548, Kluwer, 2000. https://doi.org/10.1007/978-94-011-4098-0_5

Motivation

The Hodge conjecture predicts that on a non-singular complex projective variety $X$ every rational cohomology class of type $(p,p)$ is a rational linear combination of the classes of algebraic subvarieties of $X$. Abelian varieties are the oldest testing ground for the conjecture, and the hardest known classes on them were isolated by A. Weil. A $2n$-dimensional complex abelian variety $A$ is of Weil type for an imaginary quadratic field $K=\mathbb{Q}(\sqrt{-d})$ if $K$ embeds into $\mathrm{End}_{\mathbb{Q}}(A)$ in such a way that both eigenspaces of $\eta(\sqrt{-d})$ meet $H^{1,0}(A)$ in an $n$-dimensional subspace. Such an $A$ carries a distinguished two-dimensional space of rational $(n,n)$-classes, the Weil classes, which for a generic $A$ of Weil type does not lie in the subring generated by divisor classes. Weil classes are therefore the standard obstruction to the Hodge conjecture in low dimension: for abelian fourfolds the conjecture reduces to their algebraicity.

Timeline of the unconditional results on algebraicity of Weil classes:

• A. Weil (1977) constructed the classes and showed that the generic abelian variety of Weil type has a three-dimensional space of rational $(n,n)$-classes, spanned by $h^n$ and the two-dimensional Weil plane.
• C. Schoen (Compositio Math. 65 (1988) and its 1998 Addendum, Compositio Math. 114) proved algebraicity for fourfolds of Weil type with $K=\mathbb{Q}(\sqrt{-3})$ and arbitrary discriminant, for sixfolds with $K=\mathbb{Q}(\sqrt{-3})$ and trivial discriminant, and for fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$; a second proof of the last case is in B. van Geemen's survey (1994).
• K. Koike (Canad. Math. Bull. 47 (2004)) proved algebraicity for sixfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$, which yields fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and arbitrary discriminant.
• E. Markman (JEMS 25 (2023)) proved algebraicity for fourfolds, arbitrary $K$, and discriminant $1$.
• E. Markman, arXiv:2502.03415, proves algebraicity for sixfolds of discriminant $-1$ and every imaginary quadratic $K$, and deduces the Hodge conjecture for all abelian fourfolds.

Setting

Fix $g$ and present a $g$-dimensional complex torus by its first homology: a complex structure $J$ on $H_1(A,\mathbb{R})=\mathbb{R}^{2g}$ with $J^2=-1$, the lattice being $\mathbb{Z}^{2g}\subset\mathbb{R}^{2g}$. A polarization is a rational alternating form $E$ on $H_1(A,\mathbb{Q})=\mathbb{Q}^{2g}$ satisfying the Riemann relations $E(Jx,Jy)=E(x,y)$ and $E(x,Jx)>0$ for $x\neq 0$. Cohomology is $H^k(A,\mathbb{C})=\wedge^k H^1(A,\mathbb{C})$, realized as the alternating $\mathbb{C}$-multilinear forms on $H_1(A,\mathbb{C})=\mathbb{C}^{2g}$; a class is rational if its values on rational vectors are rational, and it has type $(p,q)$ if it is multiplied by $z^p\bar z^{q}$ under the scaling action $v\mapsto (\mathrm{Re}\,z)v+(\mathrm{Im}\,z)Jv$ of $z\in\mathbb{C}$. A Hodge class of degree $2p$ is a rational class of type $(p,p)$.

Let $g=2n$ and $K=\mathbb{Q}(\sqrt{-d})$ with $d>0$. A polarized abelian $2n$-fold of Weil type is such an $(A,E)$ together with a rational endomorphism $M=\eta(\sqrt{-d})$ of $H_1(A,\mathbb{Q})$ with

$$M^2=-d,\qquad MJ=JM,\qquad E(Mx,My)=d\,E(x,y),$$

the last condition saying that $\eta(k)$ multiplies the polarization class by the norm $\mathrm{Nm}(k)$, and such that each of the two eigenspaces $W,\overline{W}\subset H_1(A,\mathbb{C})$ of $M$ meets the $i$-eigenspace of $J$ in an $n$-dimensional subspace. The Hodge–Weil classes are the rational classes in

$$\widehat{HW}\;=\;\big(\wedge^{2n}W\;\oplus\;\wedge^{2n}\overline{W}\big)\cap H^{2n}(A,\mathbb{Q}),$$

equivalently the rational degree-$2n$ classes that vanish on every tuple of vectors containing both a vector of $W$ and a vector of $\overline{W}$.

The form $H(x,y)=E(Mx,y)+\sqrt{-d}\,E(x,y)$ is $K$-valued and hermitian on $H_1(A,\mathbb{Q})$, viewed as a $K$-vector space through $\eta$. The determinant of its Gram matrix in a $K$-basis lies in $\mathbb{Q}^{\times}$, and its class in $\mathbb{Q}^{\times}/\mathrm{Nm}(K^{\times})$ is the discriminant $\det H$ of $(A,\eta,h)$. Discriminant $-1$ means that this determinant equals $-(a^2+dc^2)$ for some rationals $a,c$ not both zero.

Algebraicity is not modelled abstractly. An abelian variety is tied to a genuine non-singular projective variety $X\subseteq\mathbb{P}^N$ by a projective realization: a smooth, $\mathbb{Z}^{2g}$-periodic immersion $u:\mathbb{R}^{2g}\to X$, surjective onto $X$ and injective modulo the lattice, whose differential intertwines $J$ with the complex structure of $\mathbb{P}^N$. A class $w\in H^{2p}(A,\mathbb{C})$ is algebraic when some de Rham class of $X$ whose periods over the $2p$-cycles swept out by rational vectors $\lambda_1,\dots,\lambda_{2p}$ equal $w(\lambda_1,\dots,\lambda_{2p})$ is a rational combination of cycle classes $\mathrm{cl}(Z)$ of irreducible subvarieties $Z\subseteq X$ of dimension $g-p$. Cycle classes, de Rham cohomology of a projective variety, $(p,q)$-types and Hodge classes are taken from the platform's HodgeConjecture bundle, which formalizes §1 of Deligne's Clay problem description.

Formalization targets

Goal — Theorem 1.5.1 of arXiv:2502.03415

$$\text{For every } d>0:\ \text{the Hodge–Weil classes of a polarized abelian sixfold of Weil type with CM by }\mathbb{Q}(\sqrt{-d})\text{ and discriminant }-1\text{ are algebraic.}$$

The statement fixes neither the field $K$ nor the sixfold: it quantifies over every $d>0$, every polarized abelian sixfold of Weil type of discriminant $-1$, and every projective realization of it.

Milestone — Weil's plane of Hodge–Weil classes (§1.1)

$$\widehat{HW}\ \text{is a two-dimensional }\mathbb{Q}\text{-space, and each of its elements has type }(n,n).$$

Milestone — Schoen's degeneration step (§1.6)

$$\text{Goal for all sixfolds of discriminant }-1\ \Longrightarrow\ \text{Hodge–Weil classes of every abelian fourfold of Weil type are algebraic,}$$

for every imaginary quadratic $K$ and every discriminant; this is the use made of Schoen's Proposition 10 (Compositio Math. 114 (1998)) in the paper.

Milestone — Corollary 1.6.1

$$\text{The Hodge conjecture holds for abelian fourfolds.}$$

Milestone — Lefschetz $(1,1)$

Divisor classes: every Hodge class in $H^2$ of a non-singular projective variety is algebraic. This is an already published platform statement, imported here as a reference, since the reduction in Corollary 1.6.1 uses the algebraicity of divisor classes.

Significance

Weil classes are, by the results of Moonen–Zarhin (Duke Math. J. 77 (1995), Math. Ann. 315 (1999)), the only obstruction left in dimension four: for a simple abelian fourfold $H^{2,2}(A,\mathbb{Q})$ is spanned by quadratic expressions in divisor classes and by Weil classes, and the non-simple cases reduce to products treated by Ramón Marí (Collect. Math. 59 (2008)) and Moonen–Zarhin. The goal theorem therefore closes the Hodge conjecture for abelian fourfolds, the first dimension in which the conjecture for abelian varieties was open.

Formalizing it produces, first, a reusable Lean model of polarized abelian varieties, of complex multiplication of Weil type, of the Hodge–Weil plane and of the discriminant, tied to an honest notion of algebraic cohomology class through projective realizations. None of these objects exists in Mathlib today. The result itself is proved in the source preprint and has no machine-checked proof; the milestones below are equally unformalized, including the classical statements of Weil and Schoen that the paper's Corollary depends on.

Difficulty

The naive attack — write down subvarieties whose classes span $\widehat{HW}$ — fails because Weil classes are not expressible through divisors: for a generic abelian variety of Weil type the Néron–Severi group is cyclic while $H^{n,n}(A,\mathbb{Q})$ is three-dimensional, so no product of divisor classes reaches the Weil plane. The source constructs instead a reflexive sheaf $\mathcal{E}$ on $X\times\hat X$, for $X$ the Jacobian of a genus-$3$ curve, whose characteristic class $\kappa(\mathcal{E})$ remains of Hodge type along all deformations of $(X\times\hat X,\eta,h)$ as a polarized abelian sixfold of Weil type, and deforms the pair over that moduli space using a semiregularity theorem for twisted sheaves. Each of these steps — Orlov's derived equivalence, spinor geometry of the Mukai lattice, semiregularity — is itself missing from Mathlib, which is why the milestone list stays on the Hodge-theoretic side of the argument rather than transcribing the sheaf-theoretic core.

Formalization scope

Conventions the Lean development commits to:

1. Complex tori are presented by $(J,E)$ on $\mathbb{R}^{2g}$ with the lattice $\mathbb{Z}^{2g}$; the polarization form is rational rather than integral, which is the isogeny-invariant form of the Riemann relations.
2. Cohomology is the space of alternating multilinear forms on $H_1(A,\mathbb{C})$, i.e. invariant forms on the torus; a period over a lattice cube is used to compare it with the de Rham cohomology of a projective realization.
3. The Weil condition is imposed symmetrically on both eigenspaces of $\eta(\sqrt{-d})$, so it does not depend on the choice of convention for $H^{1,0}$ versus $H^{0,1}$.
4. Discriminant $-1$ is stated as the existence of a $K$-basis in which the Gram determinant of $H$ is $-\mathrm{Nm}(k)$; changing the basis multiplies the determinant by a norm, so the condition is basis-independent.
5. Algebraicity always refers to cycle classes of subvarieties of an actual projective variety, in the sense of Deligne's formulation, never to an abstract subspace of "algebraic" classes; in particular the goal cannot be satisfied by exhibiting a formal object, and the hypotheses are satisfiable — abelian varieties of Weil type of discriminant $-1$ exist for every $K$, and abelian varieties admit projective realizations.

A complete development needs, beyond what is drafted here: the spin representation of the Mukai lattice of an abelian $n$-fold, pure spinors and $K$-secant lines, Orlov's equivalence, Atiyah classes and semiregularity for twisted sheaves. Contributions establishing any of these, or proving the Hodge-theoretic milestones, are welcome.

Selected references

• E. Markman, Cycles on abelian $2n$-folds of Weil type from secant sheaves on abelian $n$-folds, arXiv:2502.03415. https://arxiv.org/abs/2502.03415
• A. Weil, Abelian varieties and the Hodge ring, Collected Papers III, Springer 1980, 421–429.
• C. Schoen, Hodge classes on self-products of a variety with an automorphism, Compositio Math. 65 (1988), 3–32; Addendum, Compositio Math. 114 (1998), 329–336. https://eudml.org/doc/89880
• B. van Geemen, An introduction to the Hodge conjecture for abelian varieties, Lecture Notes in Math. 1594, Springer 1994, 233–252. https://doi.org/10.1007/BFb0094425
• K. Koike, Algebraicity of some Weil Hodge classes, Canad. Math. Bull. 47 (2004), 566–572. https://doi.org/10.4153/CMB-2004-055-3
• B. Moonen, Y. Zarhin, Hodge classes and Tate classes on simple abelian fourfolds, Duke Math. J. 77 (1995), 553–581. https://doi.org/10.1215/S0012-7094-95-07717-5
• B. Moonen, Y. Zarhin, Hodge classes on abelian varieties of low dimension, Math. Ann. 315 (1999), 711–733. https://doi.org/10.1007/s002080050333
• J. Ramón Marí, On the Hodge conjecture for products of certain surfaces, Collect. Math. 59 (2008), 1–26. https://doi.org/10.1007/BF03191179
• E. Markman, The monodromy of generalized Kummer varieties and algebraic cycles on their intermediate Jacobians, J. Eur. Math. Soc. 25 (2023), 231–321. https://doi.org/10.4171/JEMS/1199
• P. Deligne, The Hodge conjecture, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/hodge.pdf