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.