Algebraic Geometry

Motivation

Deciding whether a real polynomial is non-negative on $\mathbb R^n$ is NP-hard already for quartics, and the standard computational substitute is to ask whether it is a sum of squares (SOS) of polynomials, which is a semidefinite feasibility problem. The two notions agree only in three cases, determined by Hilbert in 1888: univariate polynomials, quadratic forms, and ternary quartic forms (equivalently, polynomials of degree at most 4 in two variables). Outside those cases there are non-negative polynomials that are not SOS, among them symmetric ones: Choi and Lam exhibited a symmetric quartic form in four variables that is non-negative but not SOS.

Many polynomial optimization problems are symmetric, invariant under permutations of the variables. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) study how symmetry reduces the size of SDP relaxations. Their §5 uses the degree principle, introduced by Timofte (2003) and refined by Riener (2012), to replace one symmetric problem in $n$ variables by finitely many problems in few variables. For symmetric quartics this yields an exact SOS certificate of non-negativity in every dimension: Theorem 5.5, the goal of this mission.

Timeline:

• 1888: Hilbert shows that non-negative ternary quartic forms are sums of squares (of quadratic forms).
• 1977: Choi and Lam give a non-negative symmetric quartic form in four variables that is not SOS.
• 2003: Timofte proves the half-degree principle for symmetric polynomials (J. Math. Anal. Appl.).
• 2012: Riener refines it to semialgebraic constraints, with $r = \max\{2, \lfloor \deg f/2\rfloor, \deg g_j\}$ (J. Pure Appl. Algebra).
• 2012–2013: Riener, Theobald, Jansson Andrén and Lasserre derive Theorem 5.5.

Setting

Let $\mathbb R[X] = \mathbb R[X_1, \dots, X_n]$. A polynomial $f$ is symmetric if $f(X_{\sigma(1)}, \dots, X_{\sigma(n)}) = f$ for every permutation $\sigma$; its degree $\deg f$ is the total degree. A polynomial $p$ is a sum of squares if $p = \sum_{i=1}^k h_i^2$ for some polynomials $h_i$ in the same variables.

For symmetric $f, g_1, \dots, g_m \in \mathbb R[X]$ put

$$K = \{x \in \mathbb R^n : g_1(x) \ge 0, \dots, g_m(x) \ge 0\}, \qquad r := \max\{2, \lfloor (\deg f)/2 \rfloor, \deg g_1, \dots, \deg g_m\},$$

and let $A_r \subseteq \mathbb R^n$ be the set of points with at most $r$ distinct components.

An $r$-partition of $n$ is a vector $\omega = (\omega_1, \dots, \omega_r)$ of positive, non-increasing integers with $\omega_1 + \dots + \omega_r = n$; $\Omega$ denotes the set of all of them. For $\omega \in \Omega$,

$$f^\omega := f(\underbrace{T_1, \dots, T_1}_{\omega_1}, \dots, \underbrace{T_r, \dots, T_r}_{\omega_r}) \in \mathbb R[T_1, \dots, T_r],$$

and $K^\omega := \{t \in \mathbb R^r : g_1^\omega(t) \ge 0, \dots, g_m^\omega(t) \ge 0\}$. For $r = 2$ the partitions are $(\omega_1, \omega_2)$ with $\omega_1 \ge \omega_2 \ge 1$, $\omega_1 + \omega_2 = n$; there are $\lfloor n/2 \rfloor$ of them.

Formalization targets

Goal: Theorem 5.5 (p. 23)

For $n \ge 2$ and a symmetric $f \in \mathbb R[X_1, \dots, X_n]$ of degree $4$,

$$\big(\forall x \in \mathbb R^n:\ f(x) \ge 0\big) \iff \big(\forall \omega \in \Omega:\ f^\omega \text{ is a sum of squares in } \mathbb R[T_1, T_2]\big),$$

with $\Omega$ the set of 2-partitions of $n$.

Milestones

1. Proposition 5.1 (p. 21, quoted from Riener [33, Theorem 4.5]), the degree principle:

$$\inf_{x \in K} f(x) = \inf_{x \in K \cap A_r} f(x).$$

2. Display (5.1) (p. 22), for $r \le n$:

$$\inf_{x \in K} f(x) = \min_{\omega \in \Omega}\ \inf_{t \in K^\omega} f^\omega(t).$$

3. Hilbert's theorem (p. 23): every non-negative ternary quartic form is a sum of squares.
4. The step of the proof of Theorem 5.5 (p. 23): a polynomial in two variables of degree at most 4 is non-negative if and only if it is a sum of squares.

Significance

Theorem 5.5 turns non-negativity of a symmetric quartic in any number of variables into $\lfloor n/2 \rfloor$ semidefinite feasibility problems of fixed size, one per 2-partition, each in two variables. This is a certificate scheme that is exact, in contrast with the SOS relaxation in $n$ variables, which fails for the Choi–Lam quartic. Proposition 5.1 and (5.1) are the general mechanism behind it, and they apply to any symmetric problem whose degrees are small relative to $n$: they underlie the reduced relaxation hierarchy of Theorem 5.2 of the same paper.

All four milestones and the goal are proved results in the literature; the work is formalization. As far as a search of the platform shows, neither the degree principle nor Hilbert's ternary quartic theorem has a machine-checked statement on Prove2Me, and Mathlib has the vocabulary (MvPolynomial.IsSymmetric, IsSumSq) but neither theorem. Hilbert's theorem is a classical result of real algebraic geometry that is reusable far beyond this mission, for example in any SOS-exactness argument in low dimension.

Difficulty

The obvious route to the goal is to apply Hilbert's theorem to each $f^\omega$, and that is the whole printed proof; it gives only the direction "non-negative implies every $f^\omega$ is SOS". The converse, "every $f^\omega$ SOS implies $f$ non-negative", is not a consequence of Hilbert's theorem: it says that a symmetric quartic attains its infimum, if anywhere, on points with at most two distinct coordinate values, which is the degree principle with $r = \max\{2, \lfloor 4/2 \rfloor\} = 2$. The paper quotes the degree principle from Riener's earlier work without proof, and it is not available in Mathlib.

Hilbert's theorem itself is the hardest item. It is a statement about all non-negative quartic forms in three variables, with no symmetry to exploit, and every known proof needs substantial real algebraic geometry beyond what Mathlib provides; it is not a computation on a Gram matrix.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ; evaluation is MvPolynomial.eval; degree is totalDegree; symmetric is MvPolynomial.IsSymmetric; sum of squares is Mathlib's IsSumSq in the relevant polynomial ring (the empty sum $0$ is allowed, as on the page). An $r$-partition is encoded by its block map $b : \mathrm{Fin}\ n \to \mathrm{Fin}\ r$, required to be monotone, surjective and with non-increasing fibre sizes; this is in bijection with the page's $\Omega$, and $f^\omega$ is the substitution $X_i \mapsto T_{b(i)}$. Infima in Proposition 5.1 and (5.1) are taken in EReal, so empty feasible sets give $+\infty$ and unbounded problems give $-\infty$; no extended-real arithmetic is used.

Disclosed additions and readings, each forced by the page:

• $n \ge 2$ in Theorem 5.5. For $n = 1$ there is no 2-partition and $f = X_1^4 - 1$ is a counterexample.
• $r \le n$ in (5.1). For $r > n$ there is no $r$-partition and the right-hand side is $+\infty$.
• "Ternary quartic polynomial" is a ternary quartic form in Hilbert's theorem; the inhomogeneous reading is false.
• "Of degree 4" is "degree at most 4" in the step of the proof (milestone 4), since substitution can lower the degree; the goal keeps "degree exactly 4" as printed.

Ruled out: replacing "sum of squares" by non-negativity of $f^\omega$ (which would make the goal Proposition 5.1 alone), real-valued infima (which are $0$ on empty or unbounded sets), or arbitrary maps $\mathrm{Fin}\ n \to \mathrm{Fin}\ 2$ in place of 2-partitions.

Welcome contributions: Hilbert's theorem on ternary quartics in any standard form; homogenization and dehomogenization lemmas for MvPolynomial and IsSumSq; the degree principle, first for $K = \mathbb R^n$ (the case the goal needs) and then with constraints.

Selected references

• C. Riener, T. Theobald, L. Jansson Andrén, J. B. Lasserre, Exploiting symmetries in SDP-relaxations for polynomial optimization, Math. Oper. Res. 38(1):122–141, 2013; arXiv:1103.0486v3. https://arxiv.org/abs/1103.0486, https://doi.org/10.1287/moor.1120.0558
• C. Riener, On the degree and half-degree principle for symmetric polynomials, J. Pure Appl. Algebra 216(4):850–856, 2012. https://doi.org/10.1016/j.jpaa.2011.08.012
• V. Timofte, On the positivity of symmetric polynomial functions. Part I: General results, J. Math. Anal. Appl. 284(1):174–190, 2003. https://doi.org/10.1016/S0022-247X(03)00301-9
• D. Hilbert, Über die Darstellung definiter Formen als Summe von Formenquadraten, Math. Ann. 32:342–350, 1888. https://doi.org/10.1007/BF01443605
• M. D. Choi, T. Y. Lam, Extremal positive semidefinite forms, Math. Ann. 231:1–18, 1977. https://doi.org/10.1007/BF01360024

Motivation

Polynomial optimization asks for the minimum $f^*$ of a polynomial $f$ over a set $K\subseteq\mathbb R^n$ cut out by polynomial inequalities. Lasserre's moment relaxation (Lasserre 2001) replaces the minimization over points by a minimization over probability measures on $K$, and then over linear functionals on polynomials that satisfy semidefinite constraints. The bridge between measures and semidefinite constraints is Putinar's theorem (Putinar 1993): on a compact basic semialgebraic set with an Archimedean description, a linear functional comes from a measure exactly when it is nonnegative on the quadratic module of the constraints.

Many problems of practical size are invariant under a group of linear transformations: permutations of variables, sign changes, rotations of a polygon. Gatermann and Parrilo (2004) showed how such symmetry block-diagonalizes sums-of-squares programs. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) carry the reduction to the moment side. Their first step, Theorem 3.2, is a symmetric version of Putinar's theorem: for invariant data it suffices to consider functionals that are themselves invariant, and these are characterized by positivity of symmetrized localizing forms. This mission formalizes that theorem.

Setting

Write $\mathbb R[X]=\mathbb R[X_1,\dots,X_n]$. Let $G$ be a finite subgroup of $\mathrm{GL}_n(\mathbb R)$. A matrix $\sigma\in G$ acts on points by $x\mapsto\sigma x$ and on polynomials by

$$p^\sigma(x):=p(\sigma^{-1}x),$$

the linear substitution $X_i\mapsto\sum_j(\sigma^{-1})_{ij}X_j$. A polynomial is $G$-invariant if $p^\sigma=p$ for every $\sigma\in G$.

Fix $g_1,\dots,g_m\in\mathbb R[X]$ and the feasible set

$$K=\{x\in\mathbb R^n:\ g_j(x)\ge0,\ j=1,\dots,m\}.$$

Assumption 2.1 requires $K$ to be compact and some polynomial $u=u_0+\sum_j u_jg_j$, with sums of squares $u_0,\dots,u_m$, to have a compact superlevel set $\{u\ge0\}$. Put $g_0:=1$.

A linear map $L^G:\mathbb R[X]\to\mathbb R$ is $G$-linear if $L^G(f)=L^G(f^\sigma)$ for all $f$ and all $\sigma\in G$. Its symmetrized localizing forms are

$$\mathcal L^G_{g_j}(p,q)=L^G\Big(\frac1{|G|}\sum_{\sigma\in G}(p\cdot q)^\sigma\cdot g_j\Big),\qquad 0\le j\le m.$$

For a Borel measure $\mu$ on $\mathbb R^n$, $\mu^\sigma(B)=\mu(\sigma^{-1}(B))$ is its image under $x\mapsto\sigma x$, and $\mu$ is $G$-invariant if $\mu^\sigma=\mu$ for all $\sigma\in G$. A measure on $K$ is one with $\mu(\mathbb R^n\setminus K)=0$.

Formalization targets

Goal: Theorem 3.2

If the $g_j$ are $G$-invariant and Assumption 2.1 holds, then for a $G$-linear $L^G$: $\exists\,\mu\ \text{finite, $G$-invariant, on }K:\ \ L^G(p)=\int p\,d\mu\ \ \forall p \quad\Longleftrightarrow\quad \mathcal L^G_{g_j}(p,p)\ge0\ \ \forall p\in\mathbb R[X],\ \forall\, 0\le j\le m.$

Milestones

1. Theorem 2.2 (Putinar). Under Assumption 2.1, a linear $L$ is integration against a probability measure on $K$ iff $L(1)=1$ and $L(s_0+\sum_js_jg_j)\ge0$ for all sums of squares $s_0,\dots,s_m$.
2. Averaging identity (p. 10). For $G$-linear $L^G$: $L^G(p)=\frac1{|G|}\sum_\sigma L^G(p^\sigma)=L^G\big(\frac1{|G|}\sum_\sigma p^\sigma\big)$.
3. Only-if computation (p. 11). For a finite $G$-invariant $\mu$ on compact $K$ and invariant $g_j$: $\int\frac1{|G|}\sum_\sigma(f^2)^\sigma g_j\,d\mu=\int f^2g_j\,d\mu\ge0$.
4. If computation (p. 11). For $G$-linear $L^G$ and invariant $g$: $\mathcal L^G_g(h,h)=L^G(h^2g)$.
5. Invariance from moments (p. 11). A finite measure on compact $K$ with $\int h\,d\mu=\int h^\sigma d\mu$ for every polynomial $h$ and every $\sigma\in G$ is $G$-invariant.

Significance

The result. Theorem 3.2 turns the moment relaxation of a $G$-invariant problem into one over $G$-linear functionals. Such a functional is determined by its values on the invariant ring $\mathbb R[X]^G$, so its moment variables are indexed by a basis of invariants instead of all monomials (Example 3.3 of the paper: five variables instead of fifteen for $C_4$ on $\mathbb R^4$ in degree 2). The block-diagonalized relaxations and the convergence result of §3 (Theorems 3.4–3.7) rest on it.

Formalizing it. The theorem is proved in the paper, modulo Putinar's theorem, which is cited. Neither Putinar's theorem nor any Archimedean Positivstellensatz is in Mathlib or on the platform. A complete formalization therefore needs (i) Putinar's theorem itself, in its dual moment form, and (ii) the determinacy of compactly supported finite measures by polynomial moments in several variables. Both are reusable well beyond this paper: every moment-SOS hierarchy result in the literature cites them.

Difficulty

The group-theoretic steps (milestones 2–4) are finite averaging and change of variables. The weight of the theorem sits in two analytic facts. The first is Putinar's theorem: nonnegativity on the quadratic module is an algebraic condition, and producing a measure from it requires the Archimedean hypothesis of Assumption 2.1 in an essential way; without that hypothesis the statement is false in general. The second is that the measure Putinar's theorem returns has to be shown $G$-invariant. Equality of the polynomial moments of $\mu$ and $\mu^\sigma$ does not by itself identify two measures; it does so here because both are finite and carried by a compact set, where polynomials are dense in the continuous functions. A further detail: Putinar's theorem is stated for normalized functionals, and Theorem 3.2 is not normalized, so the degenerate case $L^G(1)=0$ must be shown to force $L^G=0$.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ, points Fin n → ℝ, and $G$ a Subgroup (GL (Fin n) ℝ) with a Fintype instance. The action on polynomials is the linear substitution aeval, so $G$ is an arbitrary finite matrix group, not only a permutation group. Sums of squares are Mathlib's IsSumSq. "psd" for the symmetric form $\mathcal L^G_{g_j}$ means $\mathcal L^G_{g_j}(p,p)\ge0$ for every polynomial $p$, with no degree truncation; $j=0$ ($g_0=1$) is included. Measures live on the Borel σ-algebra of $\mathbb R^n$, $\mu^\sigma$ is Measure.map along the continuous (hence measurable) map $x\mapsto\sigma x$, and "measure on $K$" is $\mu(\mathbb R^n\setminus K)=0$.

Committed conventions and disclosed readings:

• Finite measure. The paper writes "a $G$-invariant measure on $K$". It is formalized as a finite Borel measure; this is the reading that makes $\int p\,d\mu$ meaningful for every polynomial, and finite measures on a compact set make every polynomial integrable.
• No normalization. As on the page, Theorem 3.2 has neither $L^G(1)=1$ nor a probability measure; Theorem 2.2 has both.
• Direction of $\mu^\sigma$. With $\mu^\sigma$ the image of $\mu$ under $\sigma$, one has $\int h^\sigma d\mu=\int h\,d\mu^{\sigma^{-1}}$, where the paper writes $\int h\,d\mu^\sigma$. Statements quantify over all $\sigma\in G$, so the difference does not change their content.

Trivializing formalizations are ruled out: integrals are taken only against finite measures carried by a compact set, so no statement holds because a Bochner integral of a non-integrable function is $0$; positivity is through the forms on all of $\mathbb R[X]$, not replaced by pointwise nonnegativity; and the invariance of $\mu$ is a conclusion of milestone 5, never a hypothesis.

Contributions welcome: Putinar's theorem (milestone 1) and multivariate moment determinacy on compact sets are the reusable infrastructure; the averaging milestones are a natural first entry point.

Selected references

• C. Riener, T. Theobald, L. Jansson Andrén, J. B. Lasserre, Exploiting symmetries in SDP-relaxations for polynomial optimization, Math. Oper. Res. 38(1):122–141, 2013. arXiv:1103.0486v3, doi:10.1287/moor.1120.0558
• M. Putinar, Positive polynomials on compact semi-algebraic sets, Indiana Univ. Math. J. 42(3):969–984, 1993. doi:10.1512/iumj.1993.42.42045
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11(3):796–817, 2001. doi:10.1137/S1052623400366802
• K. Gatermann, P. A. Parrilo, Symmetry groups, semidefinite programs, and sums of squares, J. Pure Appl. Algebra 192:95–128, 2004. doi:10.1016/j.jpaa.2003.12.011

Motivation

Lasserre's hierarchy is a sequence of semidefinite relaxations for minimizing a polynomial over a set defined by polynomial equations and inequalities (Lasserre 2001). Under the archimedean condition its optimal values converge to the true minimum, but only asymptotically in general; in practice the hierarchy is often exact at a small relaxation order. J. Nie's paper (arXiv:1206.0319v2, Math. Program. 146 (2014)) explains this gap in two steps. Its Theorem 1.1 shows that finite convergence follows when the classical optimality conditions of nonlinear programming hold at every global minimizer. Its Theorem 1.2, the subject of this mission, shows that those optimality conditions hold at every local minimizer for all input data outside the zero set of finitely many polynomials in the coefficients. Together the two results give finite convergence of Lasserre's hierarchy for generic archimedean problems.

The genericity statement is also of independent interest in nonlinear programming: it says that degenerate local minimizers (failing constraint qualification, strict complementarity or second order sufficiency) are an algebraically exceptional phenomenon for polynomial data of fixed degrees.

Setting

Fix $n$ variables $x=(x_1,\dots,x_n)$ and write $\mathbb R[x]_d$ for the real polynomials of degree at most $d$. Problem (1.1) is

$$\min f(x)\quad\text{s.t.}\quad h_i(x)=0\ (i\in[m_1]),\qquad g_j(x)\ge 0\ (j\in[m_2]),$$

with feasible set $K$. For $u\in K$ the active set is $J(u)=\{j: g_j(u)=0\}$. At $u$:

• the constraint qualification condition (CQC) holds if $\nabla h_1(u),\dots,\nabla h_{m_1}(u),\nabla g_j(u)$ ($j\in J(u)$) are linearly independent;
• Lagrange multipliers $\lambda,\mu$ satisfy (1.3) $\nabla f(u)=\sum_i\lambda_i\nabla h_i(u)+\sum_j\mu_j\nabla g_j(u)$ and (1.4) $\mu_jg_j(u)=0$, $\mu_j\ge0$;
• strict complementarity (1.5) is $\mu_j+g_j(u)>0$ for all $j$;
• with $L=f-\sum_i\lambda_ih_i-\sum_{j\in J(u)}\mu_jg_j$, the second order sufficiency condition (1.7) is $v^T\nabla^2L(u)v>0$ for every $v\neq0$ orthogonal to all active constraint gradients.

The input data are the coefficient vectors of $(f,h,g)\in\mathbb R[x]_{d_0}\times\prod_i\mathbb R[x]_{d_i}\times\prod_j\mathbb R[x]_{d'_j}$; a polynomial in the coefficients is a real polynomial evaluated at that vector. The paper's Condition 4.3 lists four families of such polynomials: resultants $\mathrm{Res}$ and discriminants $\Delta$ (§2.4) of subsets of the constraints, and the polynomials $\mathscr R$ of (4.6) and $\mathscr D$ of (4.11), which detect a complex projective solution of the homogenised critical-point systems (4.5) and (4.10). Homogenisation is $\tilde p(\tilde x)=x_0^{d}p(x/x_0)$ at the nominal degree $d$, with $\tilde x=(x_0,\dots,x_n)$.

Formalization targets

Goal: Theorem 1.2

For positive degrees $d_0,d_i,d'_j$ there are polynomials $\phi_1,\dots,\phi_L$ in the coefficients such that

$$\exists\,(f,h,g)\text{ admissible with }\textstyle\prod_l\phi_l\neq0,\qquad\text{and}\qquad \prod_l\phi_l(f,h,g)\neq0\ \Longrightarrow\ \text{CQC, (1.5), (1.7) at every local minimizer of (1.1).}$$

Milestones

1. Proposition 4.1: there is $\mathscr R$ with $\mathscr R(p_0,\dots,p_k;q)=0$ iff (4.5) has a solution $0\neq\tilde x\in\mathbb C^{n+1}$; and $\mathscr R\neq0$ excludes solutions of (4.4) in $\mathbb C^n$.
2. Proposition 4.2: there is $\mathscr D$ with $\mathscr D(p_0,\dots,p_k)=0$ iff (4.10) has a solution with $\tilde x\neq0$, $y\neq0$; and $\mathscr D\neq0$ makes the KKT system (4.2) nonsingular.
3. Proposition 4.4: at $u\in K$ with multipliers satisfying (1.3) and $\mu_jg_j(u)=0$, items (a)–(d) of Condition 4.3 give at most $n-m_1$ active constraints, CQC, $\lambda_i\neq0$ and $\mu_j\neq0$ on $J(u)$, and $\det H(u)\neq0$ for $H(u)=\left[\begin{smallmatrix}\nabla^2L(u)&G(u)^T\\G(u)&0\end{smallmatrix}\right]$.
4. Lemma 4.6: at a local minimizer where $G(u)$ has full rank, (1.7) holds iff $\det H(u)\neq0$.
5. Proposition 4.5: Condition 4.3 implies CQC, strict complementarity and SOSC at every local minimizer.
6. Appendix A: $\mathscr R$ and $\mathscr D$ do not vanish identically on the input space of given positive degrees.

Significance

The theorem gives the second half of the paper's explanation of finite convergence: combined with Theorem 1.1, Lasserre's hierarchy converges in finitely many steps for all archimedean problems with input outside a proper algebraic subset. Section 5 of the paper derives further consequences, for instance that Marshall's boundary Hessian condition holds on a Zariski open set of data, and that Putinar-type certificates exist generically on the boundary of the cone of nonnegative polynomials. Beyond polynomial optimization, the statement is a precise algebraic form of the folklore that "generic nonlinear programs are nondegenerate".

The result is proved in the paper; no machine-checked version is known. A formalization fixes the exact quantifier structure (the printed statement is vacuous without a nonvanishing clause, and two items of Proposition 4.4 need an extra hypothesis), and builds reusable infrastructure: projective elimination over $\mathbb C$, homogenisation at a nominal degree, and the bordered-Hessian characterization of second order sufficiency.

Difficulty

The local part (Proposition 4.4, Lemma 4.6, Proposition 4.5) is linear algebra plus first and second order necessary conditions. The global part is not. Proposition 4.1 and 4.2 need the main theorem of elimination theory: the set of coefficient vectors for which a homogeneous (or bihomogeneous) system has a nonzero complex solution is Zariski closed, defined by polynomials in the coefficients. Mathlib has the univariate resultant only. Appendix A, which shows these polynomials do not vanish identically, has to control the homogenised systems both at finite points and at points at infinity ($x_0=0$), where only the leading forms of the data are seen. Reasoning over $\mathbb R$ alone does not suffice: the set of data whose real system is solvable is not the zero set of a polynomial.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ, points are Fin n → ℝ, and gradients and Hessians are formal partial derivatives. Homogenised polynomials have complex coefficients in n + 1 variables, variable 0 being $x_0$, and homogenisation uses the nominal degree $d$, not the actual degree. CQC is linear independence of an indexed family (repeated gradients count twice). The optimality conditions are bundled: CQC together with one multiplier pair satisfying (1.3), (1.4), (1.5) and (1.7); under CQC the multipliers are unique.

Condition 4.3 is encoded through the defining properties of Res, Δ, $\mathscr R$ and $\mathscr D$ (unsolvability of the corresponding complex projective systems) rather than through the polynomials themselves; since the goal is existential in the polynomials, this is not a weakening. Coefficient variables exist for monomials of every degree, so the goal's nonvanishing clause is asserted at an admissible input: a formal polynomial that is nonzero but vanishes on all admissible data (such as the variable of a monomial of degree $d_0+1$) does not satisfy it. Without that clause the printed theorem would be satisfied by $\phi_1=0$.

Hypotheses added to the page, each disclosed in the statements: $m_1\le n$ in Propositions 4.4 and 4.5 (Condition 4.3's standing assumption; Theorem 1.2 is stated for all $m_1$, as printed), the nonvanishing clause in Theorem 1.2, and item (a) of Condition 4.3 in Proposition 4.4 ii)–iv) (with item (b) alone, $n=1$, $g_1=x+x^2$, $g_2=-x+x^2$, $u=0$ violates CQC). Proposition 4.2's nonsingularity is asserted at all complex critical pairs.

A complete development needs projective elimination theory over $\mathbb C$ (reusable well beyond this mission), multivariate resultants and discriminants as polynomial functions of coefficients, Euler's identity for forms, and genericity facts about critical points of polynomial programs. Contributions to any of these, and direct proofs of the local milestones, are welcome.

Selected references

• J. Nie, Optimality conditions and finite convergence of Lasserre's hierarchy, Math. Program. 146 (2014); preprint arXiv:1206.0319v2, 2013. https://arxiv.org/abs/1206.0319v2, https://doi.org/10.1007/s10107-013-0680-x
• J.B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11(3) (2001) 796–817. https://doi.org/10.1137/S1052623400366802
• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977 (Theorem I.5.7A, elimination). https://doi.org/10.1007/978-1-4757-3849-0
• I. Gelfand, M. Kapranov, A. Zelevinsky, Discriminants, Resultants, and Multidimensional Determinants, Birkhäuser, 1994. https://doi.org/10.1007/978-0-8176-4771-1

Motivation

Algebraic ampleness and positivity of a smooth Hermitian metric are different kinds of positivity for a vector bundle. The target asks for one concrete family where they separate. The source manuscript presents the surrounding research claim.

Setting

The quadric surface is ℙ¹×ℙ¹. Rank-two algebraic bundles are specified by principal affine charts and regular 2×2 transition matrices. For a bundle G, E(m) is its coordinatewise m-th-power pullback twisted by the polarization O(1,1).

Formalization target

Construct G and a family E(m) such that

$$m>0\Longrightarrow E(m)\text{ is ample},\qquad m\ge m_0\Longrightarrow E(m)\text{ has no strictly Griffiths-positive smooth metric},$$

for one positive integer m₀, with the required pullback-twist identities for every positive m.

The selected formal target is OAI.QuadricCounterexample.main_theorem.

Significance and status

The assertion compares two precise positivity conditions on the same family. The goal is existential and does not provide a numerical threshold m₀. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Proving ampleness supplies projective sections, whereas excluding every positive metric is a quantified differential-geometric obstruction. Testing one candidate metric cannot settle nonexistence.

Formalization scope

The reference defines ℙ¹ as the one-point compactification of ℂ, bundles by cocycles, ampleness through symmetric sections giving a closed projective embedding, and strict positivity by a matrix Hessian expression. SourceMainTheorem retains all of these conventions. Only the published definition block and target are attached.

Selected references

• OpenAI, Ample rank-two bundles on the quadric surface without Griffiths-positive metrics, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

The permanent of an $m\times m$ matrix $X=(x_{ij})$,

$$\operatorname{per}_m(X)=\sum_{\sigma\in S_m}\prod_{i=1}^m x_{i,\sigma(i)},$$

has the same monomials as the determinant but no signs. The determinant can be computed in polynomial time; the permanent is #P-hard (Valiant, 1979). Valiant's algebraic theory makes this contrast precise: the determinant is complete for small formulas and branching programs, the permanent is complete for the class VNP, and VP ≠ VNP, the algebraic analogue of P ≠ NP, would follow if the permanent cannot be written as a determinant of polynomially larger size with affine-linear entries. Mulmuley and Sohoni's geometric complexity theory reformulates this through orbit closures, which leads to the border version of the question studied here.

Timeline

• 1979. Valiant shows that formulas reduce to determinants and that the permanent is complete for its algebraic class (doi:10.1145/800135.804419), and that computing the permanent is #P-complete (doi:10.1016/0304-3975(79)90044-6).
• 1987–1990. Linear lower bounds of order $\sqrt2\,m$: von zur Gathen (Babai–Seress bound) (doi:10.1016/0024-3795(87)90337-5), Meshulam (doi:10.1016/0024-3795(89)90465-5), Cai (doi:10.1016/0890-5401(90)90036-H).
• 2001 and 2008. Mulmuley and Sohoni propose geometric complexity theory (doi:10.1137/S009753970038715X, doi:10.1137/080718115).
• 2004. Mignon and Ressayre prove $\mathrm{dc}(\operatorname{per}_m)\ge m^2/2$ in characteristic zero via Hessian rank (doi:10.1155/S1073792804142566).
• 2010. Cai, Chen and Li extend the quadratic bound to odd characteristic (doi:10.1007/s00037-009-0284-2).
• 2012. Grenet represents $\operatorname{per}_m$ as a determinant of order $2^m-1$ (upper bound).
• 2013. Landsberg, Manivel and Ressayre prove the border bound $\mathrm{bdc}(\operatorname{per}_m)\ge m^2/2$ (doi:10.4171/CMH/292).
• 2017. Alper, Bogart and Velasco bound $\mathrm{dc}$ via the codimension of the singular locus, which is only linear for the permanent (doi:10.1007/s10208-015-9300-x); Landsberg and Ressayre prove exponential bounds for representations with symmetry (doi:10.1016/j.difgeo.2017.03.017).

Until this work the best lower bounds for both exact and border determinantal complexity of the permanent were quadratic. The source of this mission, an OpenAI preprint dated September 24, 2026, claims a cubic lower bound in the border model.

Setting

For a complex polynomial $f\in\mathbb C[x_1,\dots,x_N]$, the determinantal complexity $\mathrm{dc}(f)$ is the least positive integer $n$ with

$$f=\det\Bigl(A_0+\sum_{j=1}^N x_jA_j\Bigr),\qquad A_0,\dots,A_N\in\mathrm{Mat}_n(\mathbb C).$$

The border determinantal complexity $\mathrm{bdc}(f)$ is the least positive $n$ such that $f$ is a coefficientwise limit of such determinants of size $n$ (the size stays fixed along the sequence; the matrices are arbitrary). Clearly $\mathrm{bdc}(f)\le\mathrm{dc}(f)$.

Formalization targets

Corollary 9.3 (milestone): smooth initial forms

If $g\in\mathbb C[x_1,\dots,x_d]$, $d\ge2$, $a\in\mathbb C^d$, and the lowest nonzero homogeneous term $G_r$ of $g(a+x)$ has degree $r\ge2$ and defines a smooth projective hypersurface, then

$$\mathrm{bdc}(g)\ \ge\ \frac{(r-1)(d-1)}{4e},\qquad \mathrm{dc}(g)\ \ge\ \frac{(r-1)(d-1)}{4e}.$$

Goal: Theorem 1.1 and Corollary 9.1

For every $m\ge1408$,

$$\mathrm{bdc}(\operatorname{per}_m)\ \ge\ \frac{m^3}{5\,529\,600\,e},\qquad \mathrm{dc}(\operatorname{per}_m)\ \ge\ \frac{m^3}{5\,529\,600\,e}.$$

The constants are those stated in the paper and are not optimized. The Lean statement OAI.PermanentBorder.permanent_cubic_lower_bounds is open on the platform.

Significance

The theorem raises the exponent of the best lower bound for the permanent versus determinant problem from $2$ (Mignon–Ressayre, Landsberg–Manivel–Ressayre) to $3$, in the border model and hence also in the exact model. Through determinant reductions it also gives $\Omega(m^3)$ lower bounds on the size of affine-linear algebraic branching programs for the permanent. It remains a polynomial bound: superpolynomial determinantal complexity of the permanent, which would separate VP from VNP-type classes, is still open. The smooth-form bound of Corollary 9.3 applies to any polynomial with a smooth initial form, not only the permanent.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Formalizing it would certify the polar-degree counting argument and the coefficient-projection construction that extracts a smooth form of linear degree and quadratic dimension from the permanent.

Difficulty

The Hessian method stops at the quadratic scale: the Hessian of an order-$n$ determinant has rank at most $2n$ at a singular matrix, while the permanent's Hessian has rank at most $m^2$, so it cannot give more than $m^2/2$. Singular-locus methods give only linear bounds for the permanent because its singular locus has small codimension. A cubic bound needs an invariant that grows multiplicatively in degree and dimension, and in the border model it must survive limits, so any intersection count used must be shown to persist for a single sufficiently close determinant.

Formalization scope

• Polynomials are MvPolynomial σ ℂ; the permanent is permanentPolynomial m on variables Fin m × Fin m.
• affineMatrixPolynomial n A₀ A is $\det(A_0+\sum_v x_vA_v)$ with complex matrices.
• HasExactDeterminant n p: $n>0$ and $p$ equals such a determinant. HasBorderDeterminant n p: $n>0$ and sequences $A_0(j),A(j)$ whose determinant polynomials converge to $p$ coefficient by coefficient. Instead of defining $\mathrm{bdc}$ as a minimum, the goal states that every admissible size $n$ obeys the bound, which is equivalent.
• For the milestone, affineSubstitution a I g is $g(a+x)$, homogeneousComponent extracts $G_r$, and smoothness is stated on the affine cone: the only common zero of $G_r$ and all its partial derivatives is $0$.
• Real constants use Real.exp 1 for $e$.

A complete development needs projective smoothness and polar intersections (Bézout-type counts with simple points), adjugate and kernel-line computations for determinant pencils, and dimension estimates for matrix fibers. Contributions formalizing Lemma 2.1 (affine substitution preserves the closure), Proposition 2.2 (equivalence of border models) or Theorem 2.3 are welcome.

Selected references

• OpenAI, A cubic lower bound for border determinantal complexity of the permanent, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-cubic-lower-bound-for-border-determinantal-complexity-of-the-permanent-September-24-2026/A-cubic-lower-bound-for-border-determinantal-complexity-of-the-permanent-September-24-2026.pdf
• L. G. Valiant, Completeness classes in algebra, STOC 1979. https://doi.org/10.1145/800135.804419
• T. Mignon, N. Ressayre, A quadratic bound for the determinant and permanent problem, IMRN, 2004. https://doi.org/10.1155/S1073792804142566
• J. M. Landsberg, L. Manivel, N. Ressayre, Hypersurfaces with degenerate duals and the Geometric Complexity Theory Program, Comment. Math. Helv., 2013. https://doi.org/10.4171/CMH/292
• J.-Y. Cai, X. Chen, D. Li, Quadratic lower bound for permanent vs. determinant in any characteristic, Comput. Complexity, 2010. https://doi.org/10.1007/s00037-009-0284-2
• K. D. Mulmuley, M. Sohoni, Geometric Complexity Theory I, SIAM J. Comput., 2001. https://doi.org/10.1137/S009753970038715X
• J. Alper, T. Bogart, M. Velasco, A lower bound for the determinantal complexity of a hypersurface, Found. Comput. Math., 2017. https://doi.org/10.1007/s10208-015-9300-x
• R. Piene, Polar classes of singular varieties, Ann. Sci. ÉNS, 1978. https://doi.org/10.24033/asens.1346

Motivation: which bounded domains cover compact spaces?

A bounded symmetric domain is a bounded connected open set in $\mathbb C^m$ with, at every point, a holomorphic involution having that point as an isolated fixed point. Examples are the ball, the polydisc and the Siegel upper half-spaces in their bounded realizations. They are the universal covers of compact locally symmetric varieties, such as compact quotients of the ball, and play a central role in algebraic geometry and number theory. A classical theme in several complex variables is that a bounded domain with a large automorphism group must be very special: Wong and Rosay showed that an automorphism orbit accumulating at a strongly pseudoconvex boundary point forces the ball, and Frankel showed that convex domains with compact quotients are symmetric.

Kollár and Pardon, studying algebraic varieties whose universal cover is semialgebraic, asked the following bounded-domain question: if a bounded semialgebraic open subset of a complex affine variety admits a properly discontinuous cocompact group of biholomorphisms, must it be a bounded symmetric domain? Semialgebraicity is a finiteness condition on the shape of the domain. It does not make the boundary smooth or convex, and it imposes nothing on the group.

Timeline

• 1970 — Vey proves that a divisible generalized Siegel domain is symmetric (Ann. Sci. ÉNS 3).
• 1977 — Wong characterizes the ball by its automorphism group among strongly pseudoconvex domains (Invent. Math. 41).
• 1979 — Rosay localizes Wong's theorem to a single $C^2$ strongly pseudoconvex boundary point (Ann. Inst. Fourier 29).
• 1989 — Frankel proves that a convex hyperbolic domain with compact quotient is a bounded symmetric domain, including non-free actions (Acta Math. 163).
• 2012 — Kollár and Pardon pose the bounded semialgebraic domain question (arXiv v2, Question 25) in Algebraic varieties with semialgebraic universal cover (J. Topol. 5; arXiv:1104.2309v2).
• 2021 — Zimmer shows that a $C^{1,1}$-bounded domain covering a compact manifold is a ball (Indiana Univ. Math. J. 70).
• 2026 — An OpenAI preprint, Symmetry of semialgebraic bounded domains with compact quotient (OpenAI Math Release, September 24, 2026), claims an affirmative answer to the Kollár–Pardon question. It has not been peer reviewed, and its proof is not formally verified.

Setting

An affine variety is a reduced complex algebraic set $V\subset\mathbb C^n$, the common zero locus of a set of polynomials. A subset of $\mathbb C^n$ is semialgebraic if it is a finite Boolean combination of sets $\{p=0\}$ and $\{p>0\}$, with $p$ a real polynomial in the real and imaginary parts of the coordinates. Let $U\subseteq V$ be open in $V$, connected, semialgebraic and bounded. A map on $U$ is holomorphic if near each point it is the restriction of a holomorphic map on an open subset of $\mathbb C^n$; a biholomorphism is a homeomorphism that is holomorphic in both directions. A group $\Gamma$ acts properly discontinuously if the action is proper for the discrete topology on $\Gamma$ (finite stabilizers are allowed), and the action is cocompact if $U/\Gamma$ is compact. $U$ is smooth if each point has a neighbourhood in $U$ biholomorphic to an open subset of some $\mathbb C^m$.

Formalization targets

Goal: semialgebraic bounded domains with compact quotient are symmetric (Theorem 1.1)

Let $U$ be a nonempty connected semialgebraic bounded open subset of a complex affine variety $V\subset\mathbb C^n$, and let a group $\Gamma$ act on $U$ by biholomorphisms, properly discontinuously and with $U/\Gamma$ compact. Then

$$U\ \text{is smooth, and}\quad U\cong D\ \text{biholomorphically for some bounded symmetric domain } D\subset\mathbb C^m .$$

The goal statement is published on the platform with status Open.

Significance

The result itself. The theorem answers the Kollár–Pardon question affirmatively. The ambient variety may be singular and nonnormal, the quotient may have finite quotient singularities, and no convexity, boundary regularity or homogeneity is assumed. It shows that semialgebraicity of a single affine realization forces the classical picture: a compact quotient of a semialgebraic bounded domain is a compact quotient of a bounded symmetric domain. This complements the universal-cover classification of the companion preprint on semialgebraic universal covers of normal projective varieties.

Formalizing it. The statement only uses polynomials, real-analytic Boolean combinations, holomorphic maps on subsets of $\mathbb C^n$ and group actions, all available in Mathlib. The proof, however, draws on Nash cell decompositions, analytic discs, scaling limits of automorphisms and Vey's theorem on divisible Siegel domains, none of which is formalized. A formal development would provide reusable semialgebraic geometry and several-complex-variables infrastructure.

Difficulty

The classical rigidity arguments (Wong–Rosay, Frankel, Zimmer) need a smooth strongly pseudoconvex or convex boundary point at which rescaled automorphisms converge to a model domain. A semialgebraic boundary can have corners with several complex-normal directions, and the normal fibres can shrink at rates that depend on tangential parameters, so the naive rescaling limit can collapse to a degenerate set. Moreover $U$ is not known to be a manifold at the start, so smoothness must be proved from the group action before any differential geometry is available. The heart of the proof is a noncollapse estimate that yields a Siegel-type quadratic model $\{\operatorname{Im}w-H(z,z)\in C\}$ to which Vey's theorem applies.

Formalization scope

• $V$ is IsAffineAlgebraic, the zero set of a set of complex polynomials in Fin n → ℂ; $U\subseteq V$ is open in the subspace topology of $V$, IsConnected (hence nonempty), bounded, and semialgebraic through an inductive predicate on real polynomials in $(\operatorname{Re}z,\operatorname{Im}z)$, closed under complement and union.
• $\Gamma$ is an arbitrary group with the discrete topology acting on the subtype $U$, with ProperSMul and a compact orbit space. Each $\gamma$ acts holomorphically in the sense of local ambient analytic extension; since $\gamma^{-1}$ also acts, the elements act by biholomorphisms. A non-faithful action is allowed and is harmless, since properness forces finite stabilizers.
• IsSmooth U asks for local biholomorphisms of neighbourhoods in $U$ onto open subsets of some $\mathbb C^m$. IsBoundedSymmetricDomain D asks that $D$ be open, connected and bounded, and have at each point an involutive biholomorphism fixing it with that point isolated among its fixed points.
• The zero-dimensional case (a point) is included and is trivial, matching the source convention.
• Needed infrastructure: semialgebraic cell decomposition and selection, Montel-type compactness on singular analytic sets, analytic discs, Kobayashi/Carathéodory-type distance estimates and the structure theory of Siegel domains. Each would be reusable.

Selected references

• J. Vey, Sur la division des domaines de Siegel, Ann. Sci. École Norm. Sup. (4) 3 (1970), 479–506. https://www.numdam.org/article/ASENS_1970_4_3_4_479_0.pdf
• B. Wong, Characterization of the unit ball in $\mathbb C^n$ by its automorphism group, Invent. Math. 41 (1977), 253–257. https://doi.org/10.1007/BF01403050
• J.-P. Rosay, Sur une caractérisation de la boule parmi les domaines de $\mathbb C^n$ par son groupe d'automorphismes, Ann. Inst. Fourier 29 (1979), 91–97. https://doi.org/10.5802/aif.768
• S. Frankel, Complex geometry of convex domains that cover varieties, Acta Math. 163 (1989), 109–149. https://doi.org/10.1007/BF02392734
• J. Kollár and J. Pardon, Algebraic varieties with semialgebraic universal cover, J. Topol. 5 (2012), 199–212. https://doi.org/10.1112/jtopol/jts001
• A. Zimmer, Smoothly bounded domains covering compact manifolds, Indiana Univ. Math. J. 70 (2021), 2653–2676. https://arxiv.org/abs/1910.05288v2
• M. Coste, Real algebraic sets, lecture notes, 2005. https://indico.ictp.it/event/a04204/session/10/contribution/7/material/0/0.pdf
• OpenAI, Symmetry of semialgebraic bounded domains with compact quotient, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symmetry-of-semialgebraic-bounded-domains-with-compact-quotient-September-24-2026/paper.pdf

Motivation: when is a split tangent bundle integrable?

If a complex manifold is a product $X_1\times X_2$, its tangent bundle splits as the sum of the pulled-back tangent bundles of the factors, and each summand is integrable: the bracket of two local holomorphic vector fields tangent to a summand stays in that summand. Conversely, given a holomorphic decomposition $T_X=E_1\oplus E_2$, one wants to know whether it comes from a product. Integrability of the summands is the necessary local condition, and it can fail: Höring exhibited a non-integrable summand on the product of an abelian surface with $\mathbb P^1$ (Höring 2007, Example 2.14). For rationally connected projective manifolds — those in which two general points lie on a rational curve, a class including all Fano manifolds — Höring showed that integrability of one summand already yields a compatible product decomposition, which made automatic integrability the remaining question.

Timeline

• 2000 — Beauville studies how a tangent splitting of a compact Kähler manifold leads to a product decomposition of its universal cover (Beauville 2000).
• 2002 — Campana and Peternell treat Fano manifolds with a two-summand splitting when one summand has rank one or two, hence every two-summand splitting of a Fano manifold of dimension at most five (Campana–Peternell 2002, Theorems 3.5–3.6, Corollary 3.7).
• 2007 — Höring proves that on a rationally connected projective manifold integrability of one summand gives a compatible product (Höring 2007, Theorem 1.4).
• 2008 — Höring conjectures that at least one summand is integrable and proves it when all summands of a uniruled manifold have rank at most two (Höring 2008, Conjecture 1.2, Lemma 4.21).
• 2026 — Höring proves integrability with algebraic leaves on $\mathbb Q$-factorial klt varieties of Fano type, giving actual products in the smooth Fano case, and formulates the smooth rationally connected statement as Conjecture 1.5; a singular rationally connected counterexample shows smoothness matters (Höring 2026).
• 2026 — An OpenAI preprint, Integrability of split tangent bundles on rationally connected manifolds (OpenAI Math Release, September 23, 2026), claims this conjecture in full: both summands are always integrable. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

A complex manifold $X$ of dimension $n$ is a Hausdorff, second-countable space with a holomorphic atlas to $\mathbb C^n$. $X$ is projective if it admits an injective holomorphic immersion into a complex projective space $\mathbb P^N$; for compact $X$ this is a closed embedding.

A rational curve in $X$ is a holomorphic map $\mathbb P^1\to X$. A compact connected projective manifold is rationally connected if there is a nonempty Zariski-open set $U\subseteq X\times X$ such that every pair $(x,y)\in U$ lies on the image of a rational curve. Here Zariski-open is measured through the projective embedding: $U$ is the complement of the common zero set of a family of bihomogeneous polynomials in the two sets of homogeneous coordinates.

A holomorphic splitting $T_X=E_1\oplus E_2$ is given by a holomorphic field of idempotent linear maps $P_x$ on the tangent spaces, with $E_1=\operatorname{im}P$ and $E_2=\ker P$, both of positive rank at every point. A family of subspaces $D$ is integrable if for every open $U$ and every pair of holomorphic vector fields $V,W$ on $U$ with values in $D$, the Lie bracket $[V,W]$ takes values in $D$.

Formalization targets

Goal: Theorem 1.1 (automatic integrability)

Let $X$ be a smooth connected projective complex manifold of dimension at least two which is rationally connected. For every holomorphic decomposition $T_X=E_1\oplus E_2$ into subbundles of positive rank,

$$[\Gamma(U,E_1),\Gamma(U,E_1)]\subseteq\Gamma(U,E_1)\quad\text{and}\quad[\Gamma(U,E_2),\Gamma(U,E_2)]\subseteq\Gamma(U,E_2)$$

for every open $U\subseteq X$, where $\Gamma(U,E_i)$ denotes holomorphic sections over $U$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem has no rank or positivity hypothesis, and it settles the smooth rationally connected case of Höring's conjecture. Combined with Höring's product theorem it gives Corollary 1.2: every holomorphic splitting of the tangent bundle of a smooth rationally connected projective manifold comes from an isomorphism $X\simeq X_1\times X_2$ identifying $E_i$ with the factor tangent bundles. It also applies to general fibers of the rationally connected quotient of a uniruled compact Kähler manifold, supplying the integrability premise in Höring's structure theorems (Corollary 5.1). Together with the companion preprint on universal-cover splitting for compact Kähler manifolds, it covers both the integrability question and the global product question.

Formalizing it. The statement involves projective embeddings, Zariski-open sets of pairs, rational curves and holomorphic distributions, all expressed from first principles over Mathlib's manifold library. A machine-checked proof would certify a classical-looking but new geometric argument; the compatible product (Corollary 1.2) is not part of this goal.

Difficulty

The bracket of two sections of $E_1$, projected to $E_2$, is a tensor $\bigwedge^2E_1\to E_2$, and the task is to show it vanishes. The natural approach is to restrict to rational curves and use positivity, as in the Fano and low-rank cases, but without positivity or rank assumptions the restricted bundles can have summands of either sign and no vanishing follows directly. Smoothness cannot be dropped: a singular rationally connected example with a non-integrable summand exists (Höring 2026, Example 4.3), so the argument must use the manifold structure in an essential way. Rational connectedness is also needed: Höring's example on an abelian surface times $\mathbb P^1$ is a smooth projective manifold with a non-integrable summand.

Formalization scope

• ComplexManifold carries its dimension, a Hausdorff second-countable topology, and an analytic (ω) atlas modeled on Fin dim → ℂ. The theorem assumes ConnectedSpace, CompactSpace and 2 ≤ X.dim.
• ProjectiveEmbedding X is an injective map to ℙ ℂ (Fin (N+1) → ℂ) that is holomorphic and immersive in every affine patch.
• RationalCurve X is a holomorphic map from $\mathbb P^1$ given by two holomorphic maps $\mathbb C\to X$ agreeing via $z\mapsto z^{-1}$; RationallyConnected e asks for a nonempty, dense, Zariski-open set of pairs (bihomogeneous polynomial complement) all joined by rational curves. Density is automatic for a nonempty Zariski-open subset of the irreducible variety $X\times X$, so stating it does not narrow the class.
• TangentSplitting X is a holomorphic idempotent field on the tangent bundle with range and kernel of positive rank at every point. Integrable uses VectorField.mlieBracketWithin for sections that are holomorphic on an open set.
• The conclusion asserts integrability of both the range and the kernel; the compatible product of Corollary 1.2 is not asserted.
• Infrastructure needed: holomorphic maps from $\mathbb P^1\times\mathbb P^1$, resolution of indeterminacy for rational maps of surfaces, holomorphic bundles on $\mathbb P^1$, families of rational curves. The splitting and integrability definitions are reusable for the companion universal-cover mission.

Selected references

• A. Beauville, Complex manifolds with split tangent bundle, in Complex Analysis and Algebraic Geometry (de Gruyter, 2000), 61–70. https://arxiv.org/abs/math/9809033v2
• F. Campana, T. Peternell, Projective manifolds with splitting tangent bundle, I, Math. Z. 241 (2002), 613–637. https://doi.org/10.1007/s00209-002-0435-5
• A. Höring, Uniruled varieties with split tangent bundle, Math. Z. 256 (2007), 465–479. https://arxiv.org/abs/math/0505327v3
• A. Höring, The structure of uniruled manifolds with split tangent bundle, Osaka J. Math. 45 (2008), 1067–1084. https://www.i-repository.net/contents/osakacu/sugaku/111F0000002-04504-14.pdf
• A. Höring, Fano varieties with split tangent sheaf, preprint (2026). https://arxiv.org/abs/2602.15427v1
• J. Kollár, Y. Miyaoka, S. Mori, Rationally connected varieties, J. Algebraic Geom. 1 (1992), 429–448.
• OpenAI, Integrability of split tangent bundles on rationally connected manifolds, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integrability-of-split-tangent-bundles-on-rationally-connected-manifolds-September-23-2026/main.pdf

Motivation: Nagata's conjecture beyond the plane

Seshadri constants measure the local positivity of a line bundle at a point or a configuration of points: how much of an ample class survives after blowing up the points and subtracting equal multiples of the exceptional curves. For $r$ points on a surface with ample $L$, a dimension count gives the universal upper bound $\sqrt{L^2/r}$. Nagata's 1959 conjecture, which came out of his counterexample to Hilbert's fourteenth problem, says that this bound is attained at $r\ge10$ very general points of the projective plane. On an arbitrary polarized surface, the qualitative Nagata–Biran(–Szemberg) conjecture predicts that the bound is attained at $r$ very general points for every sufficiently large $r$. On the symplectic side, the conjecture corresponds to packing stability: large numbers of equal balls fill a four-manifold.

Timeline

• 1959 — Nagata formulates his plane conjecture and proves the strict multiplicity inequality when $r\ge16$ is a perfect square (Amer. J. Math. 81).
• 1999 — Biran proves symplectic packing stability for rational symplectic classes on closed four-manifolds (Invent. Math. 136).
• 2003 — Harbourne proves maximality for all sufficiently large $r$ with $rL^2$ a perfect square, and asymptotic lower bounds (J. reine angew. Math.).
• 2004 — Roé relates one-point and multipoint Seshadri constants (J. Algebra); Strycharz-Szemberg and Szemberg formulate a stronger prediction with an explicit threshold (Serdica Math. J. 30).
• 2009 — Roé and Ross prove a multipoint product inequality that propagates maximality (Geom. Dedicata).
• 2010 — Syzdek and Szemberg state the qualitative conjecture for arbitrary polarized surfaces (Math. Nachr. 283, Conjecture 4.3; arXiv:0709.2592).
• 2016 — Buse, Hind and Opshtein prove strong packing stability for all closed symplectic four-manifolds (Trans. AMS). Symplectic stability alone does not fix the complex structure needed for the algebraic statement (Eckl 2017, Differential Geom. Appl.).
• 2026 — An OpenAI preprint, Maximal Seshadri constants on arbitrary polarized surfaces (OpenAI Math Release, September 23, 2026), claims the qualitative conjecture for every smooth complex projective surface and every ample line bundle. It has not been peer reviewed, and its proof is not formally verified.

Setting

Let $S$ be a smooth integral complex projective surface and $L$ an ample line bundle, with self-intersection $H=L^2$. For a tuple $\mathbf p=(p_1,\dots,p_r)$ of distinct points, the multipoint Seshadri constant is

$$\varepsilon(S,L;\mathbf p)=\inf_C\frac{L\cdot C}{\sum_{i=1}^r\operatorname{mult}_{p_i}C},$$

the infimum over integral curves $C$ through at least one $p_i$. If $\pi:Y\to S$ is the blow-up at $\mathbf p$ with exceptional curves $E_1,\dots,E_r$, then $\varepsilon$ is the largest $\lambda\ge0$ such that $\pi^*L-\lambda\sum E_i$ is nef (nonnegative on every integral curve), and always $\varepsilon\le\sqrt{H/r}$. Let $U_r\subset S^r$ be the set of tuples of distinct points. A property holds at very general tuples if it fails only on a countable union of proper Zariski-closed subsets of $U_r$.

Formalization targets

Goal: eventual maximality of multipoint Seshadri constants (Theorem 1.1)

For every such $(S,L)$ there is $r_0\ge1$ such that for each $r\ge r_0$ there is a countable union $Z_r$ of proper Zariski-closed subsets of $U_r$, with $U_r\setminus Z_r\neq\varnothing$, such that for every $\mathbf p\in U_r\setminus Z_r$

$$\pi^*L-\sqrt{\tfrac{L^2}{r}}\sum_{i=1}^rE_i\ \text{ is nef on the blow-up at }\mathbf p, \qquad\text{and}\qquad \varepsilon(S,L;\mathbf p)=\sqrt{\tfrac{L^2}{r}} .$$

The threshold $r_0$ may depend on $(S,L)$ and is not explicit. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.1 settles the qualitative Nagata–Biran conjecture for all polarized complex surfaces, with no assumption that $rL^2$ is a square or that a plane constant is maximal (the hypotheses needed by Harbourne, Roé and Roé–Ross). Because the conclusion is nefness of the square-zero boundary class, it rules out every curve whose degree-to-multiplicity ratio is below $\sqrt{L^2/r}$, including curves with unequal multiplicities. Via Eckl's Kähler packing correspondence, it gives the algebraic counterpart of packing stability. The sharp plane case ($r\ge10$ in $\mathbb P^2$) is a separate companion result.

Formalizing it. The statement is built from scheme-theoretic foundations: projective surfaces, line bundles, sheaf cohomology, blow-ups by universal property, intersection numbers through Euler characteristics. A complete proof would be among the first machine-checked results about the birational geometry of surfaces. Much of the required infrastructure, such as Riemann–Roch on surfaces, finite-dimensionality of coherent cohomology and the existence of blow-ups, is not yet in Mathlib.

Difficulty

The upper bound $\varepsilon\le\sqrt{H/r}$ is an elementary jet count. Equality requires showing that no curve on the surface has too large multiplicity at the chosen points, for all multiplicity orders simultaneously. Degenerating the points to a special configuration, the usual approach in the plane, fails because the threshold in $r$ must be uniform in the jet order: the asymptotic interpolation theorems (Alexander–Hirschowitz) give thresholds depending on a fixed multiplicity bound. Arbitrary surfaces also lack the toric coordinates available on $\mathbb P^2$. The source transfers the problem to finite interpolation on an algebraic torus through a nodal divisor in $|dL|$.

Formalization scope

• Surface: an integral scheme, smooth of relative dimension $2$ over $\operatorname{Spec}\mathbb C$, with a closed immersion into some $\mathbb P^N_{\mathbb C}$ compatible with the structure maps. LineBundle: a locally free sheaf of rank one. IsAmple: the nonvanishing loci of sections of positive powers that are affine form a neighbourhood basis.
• Cohomology is Ext^n(𝒪, M) in the category of sheaves of modules, and dimensions are finrank ℂ. Then $L^2=\chi(2L)-2\chi(L)+\chi(\mathcal O)$ and $L\cdot C=\chi(L|_C)-\chi(\mathcal O_C)$, by Riemann–Roch. If cohomology were infinite-dimensional, finrank would return $0$; finite-dimensionality for projective schemes is part of what a solver must prove.
• Points are $\mathbb C$-points, the configuration space carries the Zariski topology induced from $S^r$, and very general sets are indexed by $\mathbb N$ (IsClosed, ≠ univ, with a point outside all of them).
• The multiplicity is the order of the local equation of $C$ in the local ring at $p$. The Seshadri constant is the real sInf over integral curves with positive total multiplicity.
• Nefness is expressed through a blow-up PointBlowup, characterized by its universal property, and the exceptional ideal sheaves $\mathcal O(-E_i)$. The inequality is $\pi^*L\cdot C+\sqrt{H/r}\sum_i \deg(\mathcal O(-E_i)|_C)\ge0$ for every integral curve $C$ on the blow-up.
• Needed infrastructure: coherent cohomology of projective schemes, Riemann–Roch on curves and surfaces, blow-ups of points, jets and principal parts. Contributions building any of these layers are welcome and reusable.

Selected references

• M. Nagata, On the 14-th problem of Hilbert, Amer. J. Math. 81 (1959), 766–772. https://doi.org/10.2307/2372927
• P. Biran, A stability property of symplectic packing, Invent. Math. 136 (1999), 123–155. https://doi.org/10.1007/s002220050306
• B. Harbourne, Seshadri constants and very ample divisors on algebraic surfaces, J. reine angew. Math. (2003). https://doi.org/10.1515/crll.2003.044
• J. Roé, A relation between one-point and multi-point Seshadri constants, J. Algebra (2004). https://doi.org/10.1016/j.jalgebra.2003.10.009
• B. Strycharz-Szemberg and T. Szemberg, Remarks on the Nagata conjecture, Serdica Math. J. 30 (2004), 405–430. https://www.math.bas.bg/serdica/2004/2004-405-430.pdf
• J. Roé and J. Ross, An inequality between multipoint Seshadri constants, Geom. Dedicata (2009). https://doi.org/10.1007/s10711-008-9315-4
• W. Syzdek and T. Szemberg, Seshadri fibrations of algebraic surfaces, Math. Nachr. 283 (2010), 902–908. https://arxiv.org/abs/0709.2592v1
• O. Buse, R. Hind and E. Opshtein, Packing stability for symplectic 4-manifolds, Trans. Amer. Math. Soc. (2016). https://doi.org/10.1090/tran/6802
• T. Eckl, Kähler packings and Seshadri constants on projective complex surfaces, Differential Geom. Appl. (2017). https://doi.org/10.1016/j.difgeo.2017.03.007
• OpenAI, Maximal Seshadri constants on arbitrary polarized surfaces, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Maximal-Seshadri-Constants-on-Arbitrary-Polarized-Surfaces-September-23-2026/main.pdf

Motivation

Zero sets of holomorphic functions are the basic objects of local complex-analytic geometry. In one variable they are discrete, and nothing more needs to be said; in two or more variables the zero set of a single function is a surface, a curve or a higher-dimensional object that can have singular points, such as the cusp $\{z_1^3 = z_2^2\}$ or the crossing lines $\{z_1^2 = z_2^2\}$ in $\mathbb{C}^2$. The theory of complex-analytic subvarieties describes these sets: where they are manifolds, what their dimension is, how they decompose into irreducible pieces, and how large their singular part can be. It underlies the local theory of singularities, the study of holomorphic maps and their fibres, and complex-analytic geometry more broadly (see Chirka, Complex Analytic Sets, https://doi.org/10.1007/978-94-009-2366-9, and Gunning–Rossi, Analytic Functions of Several Complex Variables).

This mission formalizes the part of this theory developed in §6.5–6.7 of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (version 4.4, 2026, https://www.jirka.org/scv/scv.pdf), culminating in the theorem that the singular set of a hypervariety (a subvariety of pure codimension one) is itself a subvariety, of dimension at most $n-2$.

Setting

Throughout, $\mathbb{C}^n$ is the space of $n$-tuples $z = (z_1, \dots, z_n)$, and a function on an open set is holomorphic if it is complex differentiable there.

A subvariety of an open set $U \subset \mathbb{C}^n$ is a set $X \subset U$ such that every point $p \in U$ has an open neighborhood $W \subset U$ and a family $\mathcal{F}$ of holomorphic functions on $W$, possibly infinite, with

$$W \cap X = \{ z \in W : f(z) = 0 \text{ for all } f \in \mathcal{F} \}.$$

The condition is imposed near every point of $U$, so a subvariety is closed in $U$.

A point $p \in X$ is a regular point of dimension $k$ if, after a permutation of the coordinates, $z = (z', z'') \in \mathbb{C}^k \times \mathbb{C}^{n-k}$, there are open sets $U' \ni p'$, $U'' \ni p''$ and a holomorphic map $g : U' \to \mathbb{C}^{n-k}$ with

$$X \cap (U' \times U'') = \{ (z', z'') : z' \in U',\ z'' = g(z') \};$$

one writes $\dim_p X = k$. The set of regular points is $X_{\mathrm{reg}}$ and the singular set is $X_{\mathrm{sing}} = X \setminus X_{\mathrm{reg}}$. The subvariety $X$ has pure dimension $d$ if $\dim_q X = d$ at every regular point $q$, and pure codimension $c$ if it has pure dimension $n - c$. A subvariety of pure codimension one is a hypervariety. The dimension of $X$ is the maximum of $\dim_q X$ over $q \in X_{\mathrm{reg}}$.

Local statements use germs. Sets $A$, $B$ have the same germ at $p$, written $(A,p) = (B,p)$, if $A \cap W = B \cap W$ for some neighborhood $W$ of $p$, and $(A,p) \subset (B,p)$ if $A \cap W \subset B \cap W$. The ring $\mathcal{O}_p$ consists of germs at $p$ of functions holomorphic near $p$, and

$$I_p(X) = \{ (f,p) \in \mathcal{O}_p : (X, p) \subset (Z_f, p) \}$$

is the ideal of germs vanishing on $X$ near $p$, where $Z_f = f^{-1}(0)$. A germ of a subvariety is reducible if it is the union of two germs of subvarieties neither of which contains the other, and irreducible otherwise.

Formalization targets

Goal: Theorem 6.6.5

For an open set $U \subset \mathbb{C}^n$ and a subvariety $X \subset U$ of pure codimension one,

$$X_{\mathrm{sing}} \text{ is a subvariety of } U \quad\text{and}\quad \dim X_{\mathrm{sing}} \le n - 2 .$$

Milestones

1. Theorem 6.5.9. For a domain $U$ and $f$ holomorphic on $U$, the zero set $Z_f$ is empty, all of $U$, or a subvariety of pure codimension one; and $(Z_f)_{\mathrm{reg}}$ is open and dense in $Z_f$.
2. Lemma 6.5.10. For a nonempty subvariety $X$, $X_{\mathrm{reg}} \neq \emptyset$; and $X_{\mathrm{reg}}$ is open and dense in $X$.
3. Theorem 6.6.1. A germ $(X,p)$ of a hypervariety equals $(Z_f, p)$ for one holomorphic $f$, and

$$I_p(X) = (f,p)\,\mathcal{O}_p .$$

4. Corollary 6.6.3. A hypervariety germ has a representative $X = X_1 \cup \cdots \cup X_k$ with each $X_\ell$ a hypervariety whose regular part is connected.
5. Proposition 6.7.3. Every germ of a subvariety is a finite union of irreducible germs of subvarieties, none contained in another.

Significance

The result itself. The goal theorem is the codimension-one case of the general statement that the singular locus of any complex-analytic subvariety is a subvariety of strictly smaller dimension (stated without proof in the book as Theorem 6.5.11). It makes induction on dimension possible for hypervarieties: removing the singular set leaves a complex manifold of dimension $n-1$, and what is removed is again analytic and smaller. In particular, a complex curve in $\mathbb{C}^2$ given by one equation has only isolated singular points. Theorem 6.6.1 says that hypervarieties are exactly the sets locally cut out by one function generating the full ideal of vanishing germs, which fails in higher codimension (Example 6.6.2 gives a codimension-two subvariety of $\mathbb{C}^6$ not cut out by two functions).

Formalizing it. To our knowledge no proof assistant library currently contains complex-analytic subvarieties of open subsets of $\mathbb{C}^n$, their regular and singular points, or local dimension. Mathlib has schemes and Zariski-closed sets, which are algebraic and do not cover analytic sets such as $\{z_2 = e^{1/z_1}\}$, and it has germs of functions and one-variable zero sets of analytic functions. The mission therefore builds the basic vocabulary of local analytic geometry, and proves its first structural theorems, from the book's proofs.

Difficulty

Being a subvariety is a local condition near every point of $U$, and the singular set is defined negatively, as the points where no coordinate projection exhibits $X$ as a graph. To show $X_{\mathrm{sing}}$ is a subvariety one has to produce holomorphic functions whose common zeros in $X$ are exactly the singular points. There is no natural finite list of them: the discriminants from one generic linear coordinate system do not suffice, because the book shows that near some regular points every fixed coordinate system sees a non-simple root (Figure 6.7). The proof needs infinitely many coordinate changes. It also needs Weierstrass preparation, the discriminant of a Weierstrass polynomial, and the principal-ideal description of Theorem 6.6.1. None of these are in Mathlib for convergent power series in several variables. The dimension bound is a separate claim: knowing that $X_{\mathrm{sing}}$ is a subvariety does not by itself exclude that it contains an $(n-1)$-dimensional manifold piece.

Formalization scope

• $\mathbb{C}^n$ is Fin n → ℂ. Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 on open sets. A domain is IsOpen U ∧ IsConnected U (nonempty).
• IsSubvariety U X includes IsOpen U and X ⊆ U; the families $\mathcal{F}$ are arbitrary sets of functions.
• A regular point uses an equivalence Fin n ≃ Fin k ⊕ Fin m for the permutation and the split into $z'$, $z''$, so no natural-number subtraction occurs.
• Dimensions and codimensions are integers: "pure codimension 1" is "every regular point has dimension $n-1$" computed in ℤ, and "$\dim X_{\mathrm{sing}} \le n-2$" is "every regular point of $X_{\mathrm{sing}}$ has dimension $\le n-2$" in ℤ. For $n = 1$ the bound is $-1$, so the singular set must be empty. For $X_{\mathrm{sing}} = \emptyset$ the bound holds vacuously, where the book's maximum over the empty set is undefined.
• Germs of sets are not quotients: GermEq and GermSubset are the relations of Definition 6.1.3. $\mathcal{O}_p$ is a Subring of Mathlib's Filter.Germ (nhds p) ℂ, and $I_p(X)$ is an Ideal of it. "Generated by $(f,p)$" is Ideal.span {(f,p)}.
• A germ of a pure-codimension-one subvariety is given by a representative subvariety $X \subset U$ with $p \in U$. The conclusions depend only on the germ.
• Lemma 6.5.10 is stated with the proviso $X \neq \emptyset$ for its first clause; without it the page's sentence is false for $X = \emptyset$.
• The goal is not trivialized by an empty or degenerate reading: the hypotheses are met by every zero set of a nonconstant holomorphic function, and the conclusion requires both the subvariety property of $X_{\mathrm{sing}}$ near every point of $U$ and the dimension bound, not merely the existence of some description of $X_{\mathrm{sing}}$.

Infrastructure a complete development needs is Weierstrass preparation and division for convergent power series in several variables, the discriminant of a Weierstrass polynomial (Theorem 6.3.3), Noetherianity of $\mathcal{O}_p$, and the Riemann extension theorem. All of them can be reused well beyond this mission. Contributions of any of these are welcome, as are proofs of the milestones independently of the goal.

Selected references

• Jiří Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026, §6.5–6.7. https://www.jirka.org/scv/scv.pdf
• E. M. Chirka, Complex Analytic Sets, Mathematics and Its Applications 46, Kluwer, 1989. https://doi.org/10.1007/978-94-009-2366-9
• Stanisław Łojasiewicz, Introduction to Complex Analytic Geometry, Birkhäuser, 1991. https://doi.org/10.1007/978-3-0348-7617-9
• Robert C. Gunning and Hugo Rossi, Analytic Functions of Several Complex Variables, Prentice-Hall, 1965; reprinted AMS Chelsea, 2009. https://bookstore.ams.org/chel-368