Algebraic Geometry

Motivation

Counting solutions of polynomial equations over finite fields is one of the oldest themes of number theory, going back to Gauss's count of points on $x^3 + 1 = y^3$ modulo a prime. In 1949 André Weil proposed a precise description of how these counts behave when the field is enlarged: for a smooth projective variety over $\mathbb F_q$, the generating function of its point counts — the zeta function — should be a rational function with integer polynomial factors, satisfy a functional equation, and have its zeros on prescribed "critical lines", in exact analogy with the Riemann hypothesis. These Weil conjectures organized several decades of work in algebraic geometry and directly motivated the construction of étale cohomology.

Timeline (as recorded in the source article, Wikipedia: Weil conjectures):

• 1924 — Artin conjectures the statements for curves.
• 1930s — Hasse proves the case of elliptic curves: $\#E(\mathbb F_{q^m}) = 1 - \alpha^m - \beta^m + q^m$ with $|\alpha| = |\beta| = \sqrt q$.
• 1948–49 — Weil proves the conjectures for curves and formulates them in all dimensions (Weil 1949).
• 1960 — Dwork proves rationality by $p$-adic methods (Dwork 1960).
• 1965 — Grothendieck, with M. Artin and Verdier, proves rationality, the functional equation and the Betti-number statement via the Lefschetz trace formula in $\ell$-adic cohomology.
• 1974 — Deligne proves the Riemann hypothesis part (Deligne 1974); in 1980 he proves a generalization for pushforwards of sheaves (Deligne 1980).

Setting

Let $k = \mathbb F_q$ be a finite field with $q$ elements and characteristic $p$. Let $X$ be a smooth projective variety of dimension $n$ over $k$: a scheme $X$ with a structure morphism $f : X \to \operatorname{Spec} k$ that is smooth of relative dimension $n$, geometrically irreducible, and admits a closed immersion into some projective space $\mathbb P^N_k$ over $k$.

For $m \ge 1$ let $\mathbb F_{q^m}$ be the extension of $k$ of degree $m$, and let

$$N_m = \#X(\mathbb F_{q^m})$$

be the number of $k$-morphisms $\operatorname{Spec}\mathbb F_{q^m} \to X$. The zeta function of $X$ is the formal power series

$$Z(X,T) = \exp\Big(\sum_{m\ge1} \frac{N_m}{m} T^m\Big) \in \mathbb Q[[T]],$$

so that $\zeta(X,s) = Z(X, q^{-s})$.

Formalization targets

Goal: the Weil conjectures (parts 1–3)

There exist integer polynomials $P_0, \dots, P_{2n}$ and multisets of nonzero complex numbers $\{\alpha_{ij}\}_j$ such that

1. Rationality.

$$Z(X,T) = \frac{P_1(T)\,P_3(T)\cdots P_{2n-1}(T)}{P_0(T)\,P_2(T)\cdots P_{2n}(T)},$$

with $P_0(T) = 1-T$, $P_{2n}(T) = 1 - q^nT$, and $P_i(T) = \prod_j (1-\alpha_{ij}T)$ over $\mathbb C$ for $1 \le i \le 2n-1$. 2. Functional equation.

$$Z\big(X, q^{-n}T^{-1}\big) = \pm\, q^{nE/2}\, T^{E}\, Z(X,T),$$

where $E = \sum_i (-1)^i \deg P_i$ is the Euler characteristic; moreover $\{\alpha_{2n-i,j}\}_j = \{q^n/\alpha_{i,j}\}_j$ as multisets. 3. Riemann hypothesis. $|\alpha_{ij}| = q^{i/2}$ for all $1 \le i \le 2n-1$ and all $j$.

Milestones

The historical partial results (Weil's theorem for curves; Dwork's rationality; Grothendieck's rationality and functional equation; Deligne's Riemann hypothesis) and the worked examples of the source (projective line, projective space, elliptic curves, the genus-2 curve $y^2 + y = x^5$ over $\mathbb F_{41}$ and the Weil polynomials of its Jacobian).

Significance

The Weil conjectures give sharp estimates $|N_m - q^{nm} - \cdots| = O(q^{m(2n-1)/2})$ for point counts, and through them bounds on exponential sums (Kloosterman sums, character sums), the Ramanujan–Petersson conjecture for holomorphic modular forms (Deligne 1971), and the hard Lefschetz theorem over finite fields. They are a standard input in analytic number theory, coding theory and cryptography.

All four statements have been proved since 1974. None of them has a machine-checked proof in Lean/Mathlib at present; Mathlib does not yet contain étale cohomology, Jacobians of curves, or the Hasse bound for elliptic curves over finite fields. This mission records faithful, compiling statements so that partial formalizations — the elementary examples, Hasse's theorem, Weil's theorem for curves via Riemann–Roch or Stepanov–Bombieri, Dwork's $p$-adic rationality proof, and eventually the cohomological proofs — can be attached to a common target.

Difficulty

The examples with a cell decomposition (projective spaces, Grassmannians) reduce to counting points in affine spaces. Beyond them, even rationality is a theorem of substance: there is no elementary formula for $N_m$, and the counts must be shown to satisfy a linear recurrence. The functional equation and the precise shape of the $P_i$ require a cohomology theory with Poincaré duality and a Lefschetz trace formula; the Riemann hypothesis requires, in addition, control of the absolute values of Frobenius eigenvalues, which in Deligne's proof uses Lefschetz pencils, monodromy and the "tensor power trick". For curves, Riemann–Roch and the Hasse–Weil bound (or Stepanov–Bombieri) suffice, but these too are absent from Mathlib.

Formalization scope

• The finite field is any k : Type with [Field k] [Finite k] [CharP k p], p prime; q = Nat.card k. Schemes live in Scheme.{0}.
• $\mathbb P^N_k$ is Proj of $k[x_0,\dots,x_N]$ graded by total degree; "projective" means a closed immersion into some $\mathbb P^N_k$ commuting with the structure maps. "Non-singular of dimension $n$" is SmoothOfRelativeDimension n f; "variety" is GeometricallyIrreducible f.
• $N_m$ counts $k$-morphisms $\operatorname{Spec} \mathbb F_{q^m} \to X$ with $\mathbb F_{q^m}$ = FiniteField.Extension k p m; $Z(X,T)$ is PowerSeries.subst of $\sum_{m\ge1} N_m T^m/m$ into PowerSeries.exp ℚ.
• Rationality is stated as an identity of power series after clearing denominators; the functional equation is stated pointwise for complex $t \neq 0$ away from the poles of both sides; $q^{nE/2}$ is a real power.
• The Euler characteristic $E$ is encoded as $\sum_i (-1)^i \deg P_i$ (the alternating sum of the Betti numbers), since Mathlib has no étale cohomology from which to define it independently.
• Part 4 (Betti numbers of a lift to characteristic zero) is not formalized: stating it requires the complex-analytic space of a variety over a number field and its singular cohomology, which Mathlib does not provide.
• The $\alpha_{ij}$ are required to be nonzero, which excludes junk factors $1 - 0\cdot T$ and junk values of $q^n/0$.

Contributions welcome: the zeta function of projective space, Hasse's theorem, point counts and Weil polynomials for the $\mathbb F_{41}$ examples, rationality for curves, and general infrastructure (Riemann–Roch for curves, Jacobians, étale cohomology).

Selected references

• Wikipedia, Weil conjectures. https://en.wikipedia.org/wiki/Weil_conjectures
• A. Weil, Numbers of solutions of equations in finite fields, Bull. Amer. Math. Soc. 55 (1949), 497–508. https://doi.org/10.1090/S0002-9904-1949-09219-4
• B. Dwork, On the rationality of the zeta function of an algebraic variety, Amer. J. Math. 82 (1960), 631–648. https://doi.org/10.2307/2372974
• P. Deligne, La conjecture de Weil. I, Publ. Math. IHÉS 43 (1974), 273–307. https://doi.org/10.1007/BF02684373
• P. Deligne, La conjecture de Weil. II, Publ. Math. IHÉS 52 (1980), 137–252. https://doi.org/10.1007/BF02684780

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

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

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

Sensitivity analysis asks how the solution of an optimization problem changes when its data move. For linear optimization the answer has been known since the 1990s: as the objective is perturbed along a fixed direction, the optimal partition (which variables can be positive at an optimum and which slacks can) stays constant on open intervals and changes only at finitely many breakpoints, and the optimal value is piecewise linear with breakpoints exactly there (Adler and Monteiro, Algorithmica 8, 1992; Jansen, Roos and Terlaky, 1993). Semidefinite optimization (SDO) is used throughout control, combinatorial relaxations and polynomial optimization, and its parametric behaviour is less regular. The optimal partition can stay constant while the optimal sets move (a nonlinearity interval), and the optimal value need not be piecewise linear.

Mohammad-Nezhad and Terlaky (Optimization 69, 2020) defined invariancy intervals, nonlinearity intervals and transition points for parametric SDO. Hauenstein, Mohammad-Nezhad, Tang and Terlaky (arXiv:1908.10499v3; Mathematics of Operations Research, 2022) prove that there are only finitely many transition points (Theorem 1, p. 8) and then compute nonlinearity intervals with numerical algebraic geometry. Finiteness is what makes a computational description possible: without it, the interior of the domain need not decompose into finitely many intervals of each kind.

Timeline:

• 1992–1993: Adler and Monteiro, and Jansen, Roos and Terlaky, start the optimal partition approach to parametric linear optimization.
• 1999: Goldfarb and Scheinberg extend the optimal partition approach to parametric SDO (Applied Numerical Mathematics 29).
• 2020: Mohammad-Nezhad and Terlaky introduce the optimal partition approach to parametric SDO (Definitions 3–5 of the present paper are taken from there).
• 2019–2022: Hauenstein, Mohammad-Nezhad, Tang and Terlaky prove that the transition points are finite (Theorem 1) and give the nonlinearity-interval algorithm.

Setting

Let $\mathbb S^n$ be the real symmetric $n\times n$ matrices with $\langle M,X\rangle=\operatorname{tr}(MX)$. Data: $A^1,\dots,A^m,C,\bar C\in\mathbb S^n$ and $b\in\mathbb R^m$. For a real parameter $\epsilon$ consider

$$(\mathrm P_\epsilon)\ \inf_X\{\langle C+\epsilon\bar C,X\rangle:\ \langle A^i,X\rangle=b_i,\ X\succeq0\},\qquad (\mathrm D_\epsilon)\ \sup_{(y,S)}\Big\{b^Ty:\ \textstyle\sum_i y_iA^i+S=C+\epsilon\bar C,\ S\succeq0\Big\}.$$

The primal feasible set $\mathcal P$ does not depend on $\epsilon$; the dual one is $\mathcal D(\epsilon)$. The optimal value function $v(\epsilon)\in\mathbb R\cup\{\pm\infty\}$ is the infimum of $(\mathrm P_\epsilon)$, its domain is $\mathcal E=\{\epsilon:\ v(\epsilon)>-\infty\}$, and the optimal sets are $\mathcal P^*(\epsilon)=\{X\in\mathcal P:\langle C+\epsilon\bar C,X\rangle=v(\epsilon)\}$ and $\mathcal D^*(\epsilon)=\{(y,S)\in\mathcal D(\epsilon):b^Ty=v(\epsilon)\}$.

Standing assumptions (p. 2): Assumption 1, the $A^i$ are linearly independent; Assumption 2, there are $X^\circ\in\mathcal P$, $(y^\circ,S^\circ)\in\mathcal D(0)$ with $X^\circ,S^\circ\succ0$.

For $\epsilon\in\operatorname{int}(\mathcal E)$, a maximally complementary optimal solution $(X^*(\epsilon),y^*(\epsilon),S^*(\epsilon))$ has $X^*(\epsilon)\in\operatorname{ri}\mathcal P^*(\epsilon)$ and $(y^*(\epsilon),S^*(\epsilon))\in\operatorname{ri}\mathcal D^*(\epsilon)$ (Definition 1). A point $\bar\epsilon\in\operatorname{int}(\mathcal E)$ is a transition point if every interval $(\bar\epsilon-\delta,\bar\epsilon+\delta)\cap\operatorname{int}(\mathcal E)$ contains an $\epsilon$ with $\operatorname{rank}X^*(\epsilon)\ne\operatorname{rank}X^*(\bar\epsilon)$ or $\operatorname{rank}S^*(\epsilon)\ne\operatorname{rank}S^*(\bar\epsilon)$ (Definition 5).

Formalization targets

Goal: Theorem 1 (p. 8)

$$\{\bar\epsilon\in\mathbb R:\ \bar\epsilon\ \text{is a transition point}\}\ \text{is finite.}$$

The statement names no bound on the number of transition points; it asserts finiteness only.

Milestones, in the order of the paper's argument

1. Remark 1 (p. 2): strictly feasible primal and dual solutions exist at every $\epsilon\in\operatorname{int}(\mathcal E)$.
2. p. 2: $\mathcal E$ is an interval with at least two points; $v$ is finite and concave on $\mathcal E$ and continuous on $\operatorname{int}(\mathcal E)$.
3. p. 2: for $\epsilon\in\operatorname{int}(\mathcal E)$, $\mathcal P^*(\epsilon)$ and $\mathcal D^*(\epsilon)$ are nonempty and compact (strong duality).
4. (1), p. 2: on $\operatorname{int}(\mathcal E)$, a primal–dual triple is optimal iff it is feasible and $XS=0$.
5. Appendix, p. 22: the ranks at relative-interior optimal points are maximal on the optimal sets.
6. (19), p. 22: $\operatorname{int}(\mathcal E)=\bigcup_{\theta+\sigma\le n}\mathcal S_{(\theta,\sigma)}$, where $\mathcal S_{(\theta,\sigma)}$ is the set of $\epsilon\in\operatorname{int}(\mathcal E)$ at which some $(X,y,S)\in\operatorname{ri}(\mathcal P^*(\epsilon)\times\mathcal D^*(\epsilon))$ has ranks $(\theta,\sigma)$.
7. p. 22: $\bar\epsilon$ is a transition point iff $\bar\epsilon\in\operatorname{bd}(\mathcal S_{(\theta,\sigma)})\cap\operatorname{int}(\mathcal E)$ for some $\theta+\sigma\le n$.
8. p. 23: every $\mathcal S_{(\theta,\sigma)}$ is a semi-algebraic subset of $\mathbb R$.
9. [Basu–Pollack–Roy, Theorem 5.22], cited p. 22: a semi-algebraic subset of $\mathbb R$ has finitely many boundary points.

Significance

The result. Theorem 1 implies that $\operatorname{int}(\mathcal E)$ is a finite union of invariancy intervals, nonlinearity intervals and transition points (p. 8). This is the structural fact behind the paper's algorithm, which follows the optimal solution along a nonlinearity interval and detects its end points, and it extends to SDO the finite-breakpoint picture of parametric linear optimization. Without finiteness, a sensitivity report would have no finite description.

Formalizing it. The theorem is proved in the paper; nothing here is open. It has no machine-checked proof that we know of. A complete development would bring parametric conic duality into Lean (the interior point condition moving along a direction, strong duality with attainment, compactness of optimal sets), and it would connect convex analysis to semi-algebraic geometry: relative interiors, ranks of positive semidefinite matrices, and the one-dimensional case of Tarski–Seidenberg. Each of these is useful beyond this paper.

Difficulty

The obvious argument says that ranks are integers between $0$ and $n$, so they can change only finitely often. That is false for arbitrary integer-valued functions on an interval: a rank pair could alternate on a sequence accumulating at a point, producing infinitely many transition points. Finiteness needs a structural reason why each level set $\mathcal S_{(\theta,\sigma)}$ is a finite union of points and intervals. That reason is semi-algebraicity. Proving it requires showing that the relative interior of the optimal set, and the parameter values where a rank is attained there, can be described by a first-order formula over the reals, and then eliminating the quantifiers. Mathlib has no Tarski–Seidenberg theorem, and the one-variable structure theorem for semi-algebraic sets (milestone 9) is itself missing.

A second difficulty is the parametric duality: strict feasibility is assumed only at $\epsilon=0$, and propagating it to all of $\operatorname{int}(\mathcal E)$ (Remark 1) uses a theorem of the alternative for SDO.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; $X\succeq0$ is PosSemidef (which includes symmetry) and $X\succ0$ is PosDef. Symmetry of $A^i$, $C$, $\bar C$ is a hypothesis of every theorem, as are Assumptions 1–2. The optimal value $v$ is an EReal infimum over $\mathcal P$, so $v=-\infty$ is represented faithfully and $\mathcal E$ is not a junk set. $\mathcal D^*(\epsilon)$ compares $b^Ty$ with the primal value $v(\epsilon)$, as printed. The relative interior is Mathlib's intrinsicInterior. Definition 1 lets $X^*(\epsilon)$ be any maximally complementary solution. The formalization removes this choice by taking the supremum of ranks over relative-interior points, and milestone 5 shows that every such point has that rank. $\mathcal S_{(\theta,\sigma)}$ uses the relative interior of the product, as printed. A subset of $\mathbb R$ is semi-algebraic when its copy in $\mathbb R^1$ is a finite union of sets $\{p=0,\ g<0\}$ with real polynomials.

Trivializing formalizations are excluded:

• ranks are taken at relative-interior points only, never at arbitrary optimal points;
• $v$ is an extended-real infimum, never a real sInf (which would make an unbounded problem look finite with value $0$);
• transition points are defined by Definition 5 itself, not as boundary points of $\mathcal S_{(\theta,\sigma)}$.

The paper also states that $\mathcal E$ is closed. Under Assumptions 1–2 this is false: $n=2$, $m=1$, $A^1=\operatorname{diag}(1,0)$, $b=1$, $C=\begin{pmatrix}0&1\\1&1\end{pmatrix}$, $\bar C=\operatorname{diag}(0,1)$ gives $\mathcal E=(-1,\infty)$. Milestone 2 omits closedness. The paper's proof of Theorem 1 does not use it.

Contributions welcome: proofs of any milestone; a semi-algebraic toolkit in Lean (closure under Boolean operations, projections from $\mathbb R^{N+1}$ to $\mathbb R$, the one-dimensional structure theorem); conic duality for standard-form SDO.

Selected references

• J. D. Hauenstein, A. Mohammad-Nezhad, T. Tang, T. Terlaky, On computing the nonlinearity interval in parametric semidefinite optimization, Mathematics of Operations Research, 2022. arXiv:1908.10499v3
• A. Mohammad-Nezhad, T. Terlaky, Parametric analysis of semidefinite optimization, Optimization 69 (2020), 187–216.
• I. Adler, R. D. C. Monteiro, A geometric view of parametric linear programming, Algorithmica 8 (1992), 161–176.
• D. Goldfarb, K. Scheinberg, On parametric semidefinite programming, Applied Numerical Mathematics 29 (1999), 361–377.
• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, Springer, 2006.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.

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 central configuration of the Newtonian $n$-body problem is a placement of $n$ point masses in which the gravitational acceleration of every body points toward the centre of mass and is proportional to its distance from it. Central configurations generate the only explicitly known solutions of the $n$-body problem (the homographic, or self-similar, motions), they are the possible limiting shapes of total collisions, and they organise the topology of the integral manifolds. Counting them is therefore a basic question of celestial mechanics.

Timeline.

• Euler (1767) and Lagrange (1772) found all central configurations of three bodies: three collinear ones and the equilateral triangle.
• Moulton (1910) showed there are exactly $n!/2$ collinear central configurations for any positive masses.
• Chazy (1918) postulated that all central configurations are nondegenerate, which would imply finiteness; Wintner (1941) stated finiteness as a conjecture.
• Palmore (1975) gave a degenerate example, refuting Chazy's postulate but not finiteness.
• Smale (1998) listed finiteness of relative equilibria for every choice of positive masses as the 6th of his problems for the 21st century.
• Hampton and Moeckel (2006) proved finiteness for $n = 4$, using heavy computer algebra (BKK theory).
• Albouy and Kaloshin (2012) gave a new proof for $n = 4$ that avoids heavy computation, and proved finiteness for $n = 5$ except possibly for masses in a codimension-2 algebraic subset of the mass space. The case $n \ge 6$, and the $n = 5$ case for the excluded masses, remain open.

Setting

Fix $n$ bodies with masses $m_1,\dots,m_n$; body $k$ sits at $(x_k,y_k)\in\mathbb R^2$. Write $x_{kl}=x_l-x_k$, $y_{kl}=y_l-y_k$ and $r_{kl}=\sqrt{x_{kl}^2+y_{kl}^2}$. A configuration with all $r_{kl}>0$ is a central configuration (normalised so that the proportionality constant is $1$) when, for every $k$,

$$\begin{pmatrix}x_k\\ y_k\end{pmatrix}=\sum_{l\ne k} m_l\, r_{kl}^{-3}\begin{pmatrix}x_k-x_l\\ y_k-y_l\end{pmatrix}.$$

These equations are invariant under rotations of the plane; imposing $y_{12}=0$ removes this freedom, and a solution with this normalisation is a positive normalized central configuration (Definition 1 of the paper; Lean: PosNormalizedCC n m).

The proof works in the complex domain. Introducing unknowns $\delta_{kl}$ (inverse distances) with $\delta_{kl}^2(x_{kl}^2+y_{kl}^2)=1$ turns the equations into the polynomial system (4) on $\mathbb C^{2n}\times\mathbb C^{n(n-1)/2}$:

$$x_k=\sum_{l\ne k} m_l\,\delta_{kl}^3\,(x_k-x_l),\qquad y_k=\sum_{l\ne k} m_l\,\delta_{kl}^3\,(y_k-y_l),\qquad y_{12}=0 .$$

A complex solution is a normalized central configuration (Lean: NormalizedCC n m), a real one if all $x_k,y_k$ are real (Lean: RealNormalizedCC n m). The potential is $U=\sum_{k<l}m_km_l\delta_{kl}$ (Lean: potential n m).

Formalization targets

Goal — Theorem 2 (planar five bodies)

There is a closed algebraic subset $A\subset\mathbb R^5$ of codimension at least $2$ such that for all masses $m\in(\mathbb R_{>0})^5\setminus A$,

$$\#\{\text{positive normalized central configurations of the planar 5-body problem with masses } m\}<\infty .$$

The exceptional set is not made explicit; only its existence and dimension bound are asserted.

Stronger — Theorem 6

The same statement with all complex solutions of system (4) in place of the positive real ones.

Four bodies — Theorems 1, 3, 4, 5

For $n=4$ and every positive masses: finitely many positive (Theorem 1, Hampton–Moeckel) and even real (Theorem 5) normalized central configurations; finitely many complex ones unless the masses satisfy explicit polynomial relations (Theorem 3) or are all equal (Theorem 4).

Tools — Lemmas 1 and 2 and an explicit example

Lemma 1 (a polynomial image of an affine variety is finite or cofinite), Lemma 2 (the potential takes finitely many values on the solution set), and the explicit mass vector $(1,2,3,4,5)$.

Significance

The result. Theorem 2 is the first finiteness result for planar central configurations of five bodies, settling Smale's 6th problem for $n=5$ for generic masses; before it, no single 5-tuple of positive masses was known to have finitely many planar central configurations. Its four-body part gives a short proof of the Hampton–Moeckel theorem, including the real (not necessarily positive) solutions.

Formalizing it. The results are proved on paper; none of them is formalized. A formal development requires affine elimination theory (Chevalley's theorem on constructible images in the form of Lemma 1), a Sard-type argument on algebraic sets (Lemma 2), and the singular-sequence analysis of Sections 3–9, which is a long case analysis of limiting diagrams together with polynomial eliminations done by computer algebra in the paper.

Difficulty

Finiteness is not a local statement: nondegeneracy fails in general (Palmore), so no implicit-function argument applies, and a continuum of solutions would have to be excluded globally. In the complex domain continua genuinely exist for some masses (Roberts' continuum with a negative mass; its sign-modified version with positive masses solves system (4)), so any proof must use the positivity of the masses in an essential way, and the exceptional mass set of Theorem 2 cannot simply be dropped with the present method.

Formalization scope

• Bodies are indexed by Fin n; the paper's bodies $1$ and $2$ are the indices 0 and 1, so the normalisation reads y 1 - y 0 = 0.
• Masses are real (and hypothesised positive) in all main theorems; in the definition of NormalizedCC they are complex, as in Section 2 of the paper. Lemma 2 carries the paper's standing hypothesis that no nonempty subset of bodies has total mass zero (NoZeroSubMass).
• A point of system (4) is a triple (x, y, δ); δ is a full n × n array constrained to be symmetric with zero diagonal, so it carries exactly the $n(n-1)/2$ unknowns $\delta_{kl}$, $k<l$. Finiteness of the solution set is unaffected by this encoding.
• "Closed algebraic subset of codimension 2 of the mass space" is encoded as the real zero locus massZeroLocus I of an ideal I of $\mathbb R[m_1,\dots,m_5]$ with ringKrullDim (ℝ[m] ⧸ I) ≤ 3. Taking $I=0$ is impossible (the quotient has dimension $5$), so the goal is not trivialised by an exceptional set equal to the whole mass space.
• Finiteness is Set.Finite of the solution set.

Useful reusable infrastructure: finite-or-cofinite images of polynomial maps on affine varieties, and basic facts on central configurations (centre of mass, the identity $I=U$).

Selected references

• A. Albouy, V. Kaloshin, Finiteness of central configurations of five bodies in the plane, Annals of Mathematics 176 (2012), 535–588. https://doi.org/10.4007/annals.2012.176.1.10
• M. Hampton, R. Moeckel, Finiteness of relative equilibria of the four-body problem, Inventiones Mathematicae 163 (2006), 289–312. https://doi.org/10.1007/s00222-005-0461-0
• S. Smale, Mathematical problems for the next century, The Mathematical Intelligencer 20 (1998), 7–15. https://doi.org/10.1007/BF03025291