Algebraic Geometry

Motivation

Hilbert's Nullstellensatz ("theorem of zeros") is the basic link between algebra and geometry. It was proved by David Hilbert in his second major paper on invariant theory in 1893, after his 1890 paper that proved the basis theorem, and it is a foundational result of algebraic geometry. It gives an algebraic criterion for when a system of polynomial equations over an algebraically closed field has a solution, and an algebraic criterion for when one polynomial vanishes wherever a given family does. Every dictionary between affine varieties and ideals — points and maximal ideals, algebraic sets and radical ideals, irreducible sets and prime ideals — is a consequence.

This mission follows the Wikipedia article Hilbert's Nullstellensatz (snapshot of 27 September 2026): its introduction, its section Formulations, the statement of Zariski's lemma from Proofs, and the first theorem of Generalizations (finitely generated algebras over Jacobson rings).

Setting

Let $k$ be a field and $K$ an algebraically closed field extension of $k$ (every non-constant polynomial over $K$ has a root in $K$). Write $k[X_1,\dots,X_n]$ for the polynomial ring in $n$ variables. A point is an $n$-tuple $a = (a_1,\dots,a_n) \in K^n$, and $f(a)$ is the value of a polynomial $f$ at $a$.

• For an ideal $J$, the algebraic set (zero locus) is $\mathrm V(J) = \{a \in K^n : f(a) = 0 \text{ for all } f \in J\}$.
• For $U \subseteq K^n$, the vanishing ideal is $\mathrm I(U) = \{p : p(a) = 0 \text{ for all } a \in U\}$.
• The radical of $J$ is $\sqrt J = \{p : p^r \in J \text{ for some } r \in \mathbb N\}$.
• For $a \in K^n$, $\mathfrak m_a = (X_1 - a_1, \dots, X_n - a_n)$ is the ideal of the point.
• A subset $W \subseteq K^n$ is irreducible (Zariski topology) if it is nonempty and is not covered by two algebraic sets without lying in one of them.
• A commutative ring is Jacobson if every radical ideal is an intersection of maximal ideals.

Formalization targets

Goal: the Nullstellensatz

If $p \in k[X_1,\dots,X_n]$ vanishes on $\mathrm V(J) \subseteq K^n$, then

$$\exists\, r \in \mathbb N,\qquad p^r \in J.$$

This is the statement of the article's section Formulations, with the coefficient field $k$ and the algebraically closed field $K$ allowed to differ.

Milestones

1. Systems of equations. Over algebraically closed $K$: a system $f_1 = \dots = f_m = 0$ has no solution in $K^n$ iff $g_1 f_1 + \dots + g_m f_m = 1$ for some $g_i$; and $f$ vanishes on all solutions iff $f^r = g_1 f_1 + \dots + g_m f_m$ for some $r$ and $g_i$.
2. Geometric form. $\mathrm I(\mathrm V(J)) = \sqrt J$.
3. Weak Nullstellensatz. A proper ideal of $k[X_1,\dots,X_n]$ has a common zero in $K^n$; algebraic closedness is needed, as $(X^2+1) \subseteq \mathbb R[X]$ shows; for $K = \mathbb C$, $n = 1$ this is the fundamental theorem of algebra: $P$ has a complex root iff $\deg P \ne 0$.
4. Correspondences. $\mathrm V$ is an order-reversing bijection from radical ideals onto algebraic sets, with inverse $\mathrm I$; $\mathrm I(\{a\}) = \mathfrak m_a$ is maximal; every maximal ideal of $K[X_1,\dots,X_n]$ is some $\mathfrak m_a$; an algebraic set $W$ is irreducible iff $\mathrm I(W)$ is prime.
5. Intersections. $\sqrt J = \bigcap_{\mathfrak m \supseteq J} \mathfrak m = \bigcap_{a \in \mathrm V(J)} \mathfrak m_a$.
6. Zariski's lemma. A field finitely generated as an algebra over a field $K$ is a finite extension of $K$.
7. Jacobson rings. A finitely generated algebra $S$ over a Jacobson ring $R$ is Jacobson, and for a maximal ideal $\mathfrak n \subseteq S$, $\mathfrak n \cap R$ is maximal and $S/\mathfrak n$ is finite over $R/(\mathfrak n \cap R)$.

Significance

The Nullstellensatz makes the zero sets of polynomial systems accessible through ideals: solvability of a system becomes the ideal-membership question $1 \in J$, and the geometry of algebraic sets becomes the algebra of radical ideals. Consequences include the identification of the points of $K^n$ with the maximal ideals of $K[X_1,\dots,X_n]$, the description of irreducible algebraic sets by prime ideals, and the reduction of the fundamental theorem of algebra to the case $n=1$. The Jacobson-ring version extends the first equality of the intersection formula to every finitely generated algebra over a field.

All statements here are classical and proved. Mathlib already contains versions of several of them in its own vocabulary (Jacobson rings, Zariski's lemma, and a Nullstellensatz over an algebraically closed coefficient field). What this mission adds is a single set of statements matching the article's formulations: the version with separate fields $k \subseteq K$, the explicit systems-of-equations form, the point-ideal and irreducibility correspondences over $K^n$, and the intersection formula — and, for solvers, the bridges from these concrete statements to Mathlib's abstract ones.

Difficulty

The inclusion $\sqrt J \subseteq \mathrm I(\mathrm V(J))$ is immediate; the content is the reverse inclusion, which requires producing a point of $K^n$ from purely algebraic data. When $k \ne K$ the ideal $J$ lives over $k$ while the points live over $K$, so a result stated only for $K[X_1,\dots,X_n]$ does not apply directly: an ideal of $k[X]$ must be related to the ideal it generates in $K[X]$ without losing membership information. For the correspondences, the explicit ideals $\mathfrak m_a$ and the closed-set definition of irreducibility must be matched with the abstract notions (maximal spectrum, irreducible closed subsets) used in the library.

Formalization scope

• Points of $K^n$ are functions $\mathrm{Fin}\,n \to K$; polynomials are MvPolynomial (Fin n) k. When $k \ne K$, $K$ is a $k$-algebra and evaluation of a polynomial over $k$ at a point of $K^n$ goes through $k \to K$.
• $n = 0$ is allowed throughout; so is the unit ideal $J = k[X]$, where $\mathrm V(J) = \emptyset$ and empty intersections of ideals are the whole ring.
• Irreducibility is stated through closed sets (algebraic sets) without putting a topology on $K^n$. The degree in the $n=1$ statement is Mathlib's Polynomial.degree, with $\deg 0 = -\infty$.
• In the goal, the exponent $r$ may be $0$; that witness only works when $J$ is the unit ideal, so it does not trivialize the statement.
• Out of scope: the proofs via resultants and Gröbner bases, the effective Nullstellensatz, Lang's infinite-variable version, the scheme-theoretic generalizations, and the projective and analytic Nullstellensätze.
• Reusable output: the definitions $\mathrm V$, $\mathrm I$, algebraic set, irreducible set and $\mathfrak m_a$, and bridges to Mathlib's MvPolynomial.zeroLocus, MvPolynomial.vanishingIdeal, and IsJacobsonRing.

Selected references

• D. Hilbert, Ueber die vollen Invariantensysteme, Mathematische Annalen 42 (1893).
• Wikipedia contributors, Hilbert's Nullstellensatz. https://en.wikipedia.org/wiki/Hilbert%27s_Nullstellensatz
• M. F. Atiyah, I. G. Macdonald, Introduction to Commutative Algebra, Addison-Wesley, 1969, Chapters 5 and 7.
• D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Springer GTM 150, 1995, Chapter 4.

Motivation

Noetherian schemes are the standard finiteness condition of algebraic geometry. Almost every scheme met in practice is Noetherian: affine and projective varieties over a field, schemes of finite type over $\mathbb Z$, and many moduli spaces. Many basic theorems about schemes (finiteness of irreducible components, quasi-compactness of morphisms, good behaviour of coherent sheaves and their cohomology) are proved under a Noetherian hypothesis, so the notion appears in the hypotheses of a large part of the literature, starting with Hartshorne's Algebraic Geometry, Chapter II, and the Stacks Project.

This mission formalizes the foundational statements in the Wikipedia article "Noetherian scheme": the definition and its equivalent forms, the basic topological and ring-theoretic consequences, the stability of the notion under morphisms of finite type, and the standard non-examples.

Setting

A scheme $X$ is a locally ringed space that is locally isomorphic to spectra of commutative rings. For an open subset $U \subseteq X$ write $\Gamma(X,U) = \mathcal O_X(U)$ for its ring of sections. An open subset $U$ is an open affine if $U \cong \operatorname{Spec} A$ for a commutative ring $A$; then $A \cong \Gamma(X,U)$.

• $X$ is locally Noetherian if every point of $X$ lies in an open affine $U$ with $\Gamma(X,U)$ a Noetherian ring (NoetherianScheme.IsLocallyNoetherianScheme).
• $X$ is Noetherian if $X = U_1 \cup \dots \cup U_n$ for finitely many open affines $U_i$ with each $\Gamma(X,U_i)$ Noetherian (NoetherianScheme.IsNoetherianScheme).

A topological space is a Noetherian space if every descending chain of closed subsets stabilizes. A morphism $f : X \to S$ is quasi-compact if preimages of quasi-compact opens are quasi-compact, locally of finite type if it is given locally by finitely generated algebras, and of finite type if it is both.

Formalization targets

Goal

$$X \text{ Noetherian} \iff X \text{ quasi-compact and } \Gamma(X,U) \text{ Noetherian for every open affine } U \subseteq X.$$

This combines the article's statements that a scheme is Noetherian iff it is locally Noetherian and compact, and that every open affine of a locally Noetherian scheme has a Noetherian ring of sections. It shows the definition does not depend on the chosen cover.

Milestones

1. $X$ Noetherian $\iff$ $X$ locally Noetherian and compact.
2. If $X$ is locally Noetherian and $U \subseteq X$ is any open affine, then $\Gamma(X,U)$ is Noetherian.
3. $\operatorname{Spec} A$ is Noetherian $\iff$ $A$ is a Noetherian ring.
4. If $X$ is locally Noetherian, every local ring $\mathcal O_{X,x}$ is Noetherian.
5. A Noetherian scheme is a Noetherian topological space.
6. The converse fails: there is a non-Noetherian valuation ring $R$ such that $\operatorname{Spec} R$ is a Noetherian space but not a Noetherian scheme.
7. A Noetherian scheme has finitely many irreducible components.
8. Every morphism $X \to S$ with $X$ Noetherian is quasi-compact.
9. If $f : X \to S$ is locally of finite type and $S$ is locally Noetherian, then $X$ is locally Noetherian.
10. If $f : X \to S$ is of finite type and $S$ is Noetherian, then $X$ is Noetherian.
11. The adele ring $\mathbb A_K$ of a number field $K$ is not Noetherian.
12. The ring of integers of $\mathbb Q(\mu_\infty)$ (all roots of unity adjoined) is not Noetherian and has Krull dimension $1$.

Significance

The goal is what makes the notion usable: it allows checking Noetherianity on any affine cover and using it on every affine open. Milestones 1–5 and 7–8 are the facts invoked whenever a Noetherian hypothesis is used. Milestones 9–10 are the source of most examples, since they show that every scheme of finite type over a field or over $\mathbb Z$ is Noetherian. Milestones 6, 11 and 12 show the limits of the notion: Noetherianity is not a topological property, and natural rings in number theory (adeles, rings of integers of infinite extensions) fall outside it, even in dimension one.

Mathlib already contains its own versions of several of these facts, phrased through AlgebraicGeometry.IsLocallyNoetherian and AlgebraicGeometry.IsNoetherian, which take "every open affine has Noetherian sections" as the definition. The statements here use the source's cover-based definition, so connecting the two is part of the work.

Difficulty

The central point of the goal is that a cover-based condition must be transferred to an arbitrary open affine $U$, which in general is not one of the covering opens and is not covered by finitely many standard opens of a single covering affine. The obvious argument (intersect $U$ with the cover) produces opens that are not affine, or are affine in different rings, so a local-to-global argument for the property "Noetherian" on affine opens is needed. The non-examples (milestones 6, 11, 12) each require building or analysing a specific non-Noetherian ring that Mathlib does not yet study from this angle.

Formalization scope

• Schemes are Mathlib's AlgebraicGeometry.Scheme in a fixed universe u. Open affines are X.affineOpens; rings of sections are Γ(X, U); local rings are stalks X.presheaf.stalk x.
• "Covered by $\operatorname{Spec} A$ with $A$ Noetherian" is encoded as "covered by affine opens whose rings of sections are Noetherian", using $A \cong \Gamma(X,U)$. The empty scheme is Noetherian.
• "Compact" means Mathlib's CompactSpace on the underlying space (quasi-compact, no Hausdorff condition).
• Morphisms of finite type are written as LocallyOfFiniteType f together with QuasiCompact f.
• The adele ring is Mathlib's NumberField.AdeleRing (𝓞 K) K. The field $\mathbb Q(\mu_\infty)$ is any field $K$ of characteristic zero with IsCyclotomicExtension {n | 0 < n} ℚ K; such fields exist (for example inside an algebraic closure of $\mathbb Q$), so the hypothesis is not vacuous.
• Milestone 6 is an existence statement in the lowest universe, because not every non-Noetherian valuation ring has a Noetherian spectrum.
• A formalization that simply reuses Mathlib's IsNoetherian as the definition would make the goal close to a restatement; the definitions here deliberately follow the source.
• Not included: the sections on dévissage, Čech and sheaf cohomology, compatibility of cohomology with colimits, derived direct images, quasi-projective varieties, infinitesimal deformations, the maximal unramified extension example and the infinite polynomial-ring quotient. These need coherent sheaves, sheaf cohomology and derived categories of schemes, which are not yet available in Mathlib in the required form, and several of their formulas are not legible in the supplied copy of the source. They are candidates for follow-up missions.

Selected references

• Wikipedia, Noetherian scheme, revision 1372079294. https://en.wikipedia.org/w/index.php?title=Noetherian_scheme&oldid=1372079294
• R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977. https://doi.org/10.1007/978-1-4757-3849-0
• The Stacks Project, Lemma 28.5.7 (Tag 0BA8), Lemma 28.5.8 (Tag 01P0), Lemma 29.15.6 (Tag 01T6). https://stacks.math.columbia.edu
• B. Conrad, Weil and Grothendieck approaches to adelic points. http://math.stanford.edu/~conrad/papers/adelictop.pdf

Motivation

A hypersurface can be abstractly affine space without its defining equation being an ambient coordinate. Distinguishing these two properties is the embedding question behind the Abhyankar–Sathaye problem. The source manuscript presents the surrounding research claim.

Setting

For n ≥ 4, let R=ℂ[X₀,…,Xₙ₋₁]. A polynomial F is a coordinate if a ℂ-algebra automorphism of R sends some variable Xᵢ to F. Its zero fiber is represented by the quotient R/(F).

Formalization target

For every n ≥ 4, find F with

$$R/(F)\cong_{\mathbb C}\mathbb C[X_0,\ldots,X_{n-2}],\qquad F\text{ is not a coordinate}.$$

The source supplies an explicit construction, while this selected goal asks for existence.

The selected formal target is OAI.AbhyankarSathaye.exists_noncoordinate_polynomial.

Significance and status

The target separates the intrinsic affine-space quotient from ambient polynomial equivalence in every dimension at least four. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

An isomorphism of the quotient rings need not extend to an automorphism of the ambient ring. Both the quotient isomorphism and the failure of every possible coordinate automorphism must be established.

Formalization scope

The goal uses multivariate polynomials indexed by Fin n, a principal ideal, and ℂ-algebra equivalences. A separate published derivation target and its explicit polynomial definitions are retained as related references. That target concerns n−1 commuting locally nilpotent derivations, their common kernel and ordinary extra-variable partial derivatives; it is not asserted as a logical dependency of the existence goal.

Selected references

• OpenAI, An explicit noncoordinate polynomial with affine three-space zero fibre, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Logarithmic Kodaira dimension measures the supply of pluricanonical forms allowed poles along a boundary. Its behavior in a fibration depends especially on the case where a general fiber has no such nonzero forms. The source manuscript presents the surrounding research claim.

Setting

A stratum-smooth fibration is a surjective connected-fiber morphism of smooth projective complex varieties with reduced simple-normal-crossing boundaries E and D. The pullback of the base boundary is supported in E; the total space and every boundary stratum are smooth away from D.

Formalization target

Very generally on the base, the point lies outside D and every supplied fiber model F satisfies

$$\kappa(F)=-\infty\Longrightarrow\kappa(E)=\kappa(D)+\kappa(F),$$

with every positive-degree logarithmic pluriform section on the total space equal to zero.

The selected formal target is OAI.ReverseLogKodaira.SmoothProjectiveVariety.veryGenerally_fiber_negative_branch.

Significance and status

This is the fiber-negative branch of the manuscript’s wider additivity claim. Its vanishing assertion is part of the goal, not merely explanatory background. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The conclusion concerns all positive tensor degrees and every fiber model over very general points. One fixed fiber or one vanishing space of sections would not suffice.

Formalization scope

The definitions use schemes over ℂ, ideal-sheaf boundaries, exterior powers of Kähler differentials, and rational pluriform lattices. Kodaira dimension takes values in WithBot ℕ∞. Very generally means outside a countable family of proper closed subsets. The nonnegative branches and full reverse inequality are not additional attached targets.

Selected references

• OpenAI, The reverse logarithmic Kodaira inequality and additivity, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Birational anabelian geometry studies how much of a function field is determined by a small quotient of its absolute Galois group. This mission isolates uniqueness in the reconstruction correspondence. The source manuscript presents the surrounding research claim.

Setting

Fix a prime ℓ. The fields K/k and L/l are essentially finite type extensions of algebraically closed constant fields, have transcendence degree at least two, and have characteristic different from ℓ. The abelian-by-central datum records the pro-ℓ abelian quotient and the commutator pairing. IsomF consists of constant-preserving perfect-closure isomorphisms modulo Frobenius; IsomCUnits quotients bracket-compatible Galois isomorphisms by the encoded ℓ-adic unit relation.

Formalization target

For field-isomorphism classes a and a′ and a Galois-isomorphism class b, prove

$$\operatorname{PhiGraph}(a,b)\;\land\;\operatorname{PhiGraph}(a^{\prime},b)\quad\Longrightarrow\quad a=a^{\prime}.$$

PhiGraph is the relation induced by representatives and a compatible extension to algebraic closures.

The selected formal target is OAI.BogomolovPop.main_graph_injective.

Significance and status

This establishes uniqueness of the field class whenever two representatives produce the same Galois class. The manuscript states a full reconstruction bijection; the selected published Lean target is its graph-injectivity assertion. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Equality is required after two different quotient constructions, one generated by Frobenius and one by ℓ-adic scalar limits. Recovering equality of classes must respect both ambiguities and the contravariant Galois action.

Formalization scope

The definition block constructs topological pro-ℓ quotients, closed commutator subgroups, perfect closures and the pullback graph. The theorem quantifies over arbitrary field types with the stated algebraic instances. It does not assert existence, surjectivity or functionality of PhiGraph, and those broader manuscript conclusions are not attached as proved results. Only the existing injectivity target and its definition block are referenced.

Selected references

• OpenAI, The Bogomolov-Pop reconstruction theorem, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation: plethysm, Foulkes' conjecture and the canonical map

Plethysm — decomposing $\operatorname{Sym}^a(\operatorname{Sym}^b V)$ into irreducible $\mathrm{GL}(V)$-representations — is one of the oldest open problems in the representation theory of the general linear group, and it is central to geometric complexity theory, where the coordinate rings of Chow varieties of products of linear forms control lower-bound arguments. Foulkes' conjecture (1950) predicts that for $a\le b$ there is a $\mathrm{GL}(V)$-equivariant injection $\operatorname{Sym}^a(\operatorname{Sym}^bV)\hookrightarrow\operatorname{Sym}^b(\operatorname{Sym}^aV)$. A natural candidate is supplied by a specific map, the canonical Foulkes–Howe map $\mu_{a,b,V}:\operatorname{Sym}^b(\operatorname{Sym}^aV)\to\operatorname{Sym}^a(\operatorname{Sym}^bV)$; its surjectivity yields such an embedding by complete reducibility. Its image is the degree-$b$ part of the coordinate ring of the Chow variety of decomposable $a$-forms, so surjectivity for large $b$ is a statement about that variety's normalization. The question is from which degree $b$ on the map is surjective, uniformly in $\dim V$.

Timeline

• 1950 — Foulkes formulates the plethysm comparison (Foulkes, J. London Math. Soc. 1950).
• 1993 — Brion proves eventual surjectivity of the canonical map for fixed $a$ and $V$ (Brion, Manuscripta Math. 1993); in 1997 he gives an effective bound depending on both $a$ and $\dim V$ (Séminaires et Congrès 2, SMF, 1997, Theorem 3.3).
• 2008 — McKay proves a propagation theorem for Foulkes-type injectivity (J. Algebra 2008); Ikenmeyer gives a weight-shift proof (arXiv:1509.04957, 2015).
• 2015 — Landsberg's introduction to geometric complexity theory asks for a polynomial stabilization bound (Problem 7.19) (Ann. Univ. Ferrara 2015).
• 2017 — Cheung, Ikenmeyer and Mkrtchyan show that the canonical map has nonzero kernel at $(a,b)=(5,5)$ and $(6,6)$ in suitable dimensions (J. Symbolic Comput. 2017).
• 2022 — Raicu, Sam and Weyman bound the regularity of the Segre ring and modules of covariants on the Chow variety (Vietnam J. Math. 2022), without computing the top degree controlling stabilization.
• 2026 — An OpenAI preprint, Quadratic stabilization of the canonical Foulkes–Howe map (OpenAI Math Release, September 25, 2026), claims surjectivity for all $a\ge2$, $b\ge a(a-1)$ and every finite-dimensional $V$. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Let $V$ be a finite-dimensional complex vector space and $\operatorname{Sym}V$ its symmetric algebra. $\operatorname{Sym}^nV\subseteq\operatorname{Sym}V$ is the span of products $v_1\cdots v_n$ of $n$ vectors. For $v_{j,i}\in V$ ($1\le j\le b$, $1\le i\le a$), the canonical Foulkes–Howe map is the linear map determined by

$$\mu_{a,b,V}\Bigl(\prod_{j=1}^{b}\bigl(v_{j,1}\cdots v_{j,a}\bigr)\Bigr) =\frac{1}{(a!)^{b}}\sum_{\sigma_1,\dots,\sigma_b\in S_a}\ \prod_{i=1}^{a}\Bigl(\prod_{j=1}^{b}v_{j,\sigma_j(i)}\Bigr),$$

where the outer products on the left and right are taken in $\operatorname{Sym}(\operatorname{Sym}^aV)$ and $\operatorname{Sym}(\operatorname{Sym}^bV)$ respectively. Equivalently: identify $\operatorname{Sym}^aW$ with symmetric tensors via averaging, multiply $b$ such tensors in $(\operatorname{Sym}V)^{\otimes a}$, and project back. That this formula is well defined on $\operatorname{Sym}^b(\operatorname{Sym}^aV)$ is part of the content.

Formalization targets

Goal: quadratic stabilization (Theorem 1)

For every finite-dimensional complex $V$ and integers $a\ge2$, $b\ge a(a-1)$, there is a unique linear map

$$\mu:\operatorname{Sym}^b(\operatorname{Sym}^aV)\longrightarrow\operatorname{Sym}^a(\operatorname{Sym}^bV)$$

satisfying the displayed formula on monomials, and $\mu$ is surjective.

The bound $a(a-1)$ is not claimed to be sharp; the content is a stabilization degree polynomial in $a$ and independent of $\dim V$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Surjectivity gives, by complete reducibility, a $\mathrm{GL}(V)$-equivariant embedding $\operatorname{Sym}^a(\operatorname{Sym}^bV)\hookrightarrow\operatorname{Sym}^b(\operatorname{Sym}^aV)$ for $b\ge a(a-1)$ (Corollary 4 of the source), e.g. the sixth-power comparison for $b\ge30$. It answers positively the request for a polynomial bound in Landsberg's Problem 7.19, and it says that the coordinate ring of the Chow variety of decomposable $a$-forms agrees with its normalization in every degree $b\ge a(a-1)$. Since the canonical map is known to fail to be injective at $(5,5)$ and $(6,6)$, an explicit range of surjectivity is the right kind of statement for this specific map.

Formalizing it. The statement is purely algebraic and uniform in $V$, $a$, $b$. A formal proof would need multilinear algebra over symmetric algebras (symmetric powers of symmetric powers), which is reusable for plethysm and invariant-theory projects.

Difficulty

Surjectivity is equivalent to the vanishing of every symmetric $a$-linear form on $\operatorname{Sym}^bV$ whose diagonal vanishes on products of $b$ vectors. The naive induction on $a$ fails because the factors in different slots share a common product and cannot be varied independently; the dimension of $V$ also grows the space of such forms without bound, so arguments using a fixed basis or dimension count do not give a uniform bound. Brion's effective bound depends on $\dim V$, and regularity bounds for the normalization do not locate the top degree of the quotient that controls stabilization.

Formalization scope

• $\operatorname{Sym}^nV$ is represented as the submodule SymPow n V of Mathlib's SymmetricAlgebra ℂ V spanned by products of $n$ vectors, and $\operatorname{Sym}^b(\operatorname{Sym}^aV)$ is SymPow b (SymPow a V).
• IsFoulkesMap a b V μ states the monomial formula above, with the normalizing factor $(a!)^{-b}$ and the sum over $b$-tuples of permutations of Fin a.
• The goal asserts existence, surjectivity and uniqueness of a linear map with this formula; uniqueness rules out choosing an arbitrary surjection, so the theorem is about the canonical map and not merely about dimensions.
• $V$ ranges over all finite-dimensional complex vector spaces in an arbitrary universe; $a\ge2$ and $b\ge a(a-1)$ are natural numbers.
• Needed infrastructure: symmetric powers inside the symmetric algebra, polarization/annihilator criteria, and directional-derivative operators on polynomial functions.

Selected references

• H. O. Foulkes, Concomitants of the quintic and sextic up to degree four in the coefficients of the ground form, J. London Math. Soc. 25 (1950), 205–209. https://doi.org/10.1112/jlms/s1-25.3.205
• M. Brion, Stable properties of plethysm: on two conjectures of Foulkes, Manuscripta Math. 80 (1993), 347–371. https://doi.org/10.1007/BF03026558
• M. Brion, Sur certains modules gradués associés aux produits symétriques, Séminaires et Congrès 2, SMF, 1997, 157–183. https://smf.emath.fr/publications/sur-certains-modules-gradues-associes-aux-produits-symetriques
• T. McKay, On plethysm conjectures of Stanley and Foulkes, J. Algebra 319 (2008), 2050–2071. https://doi.org/10.1016/j.jalgebra.2007.12.003
• C. Ikenmeyer, On McKay's propagation theorem for the Foulkes conjecture, arXiv:1509.04957, 2015. https://arxiv.org/abs/1509.04957v1
• J. M. Landsberg, Geometric complexity theory: an introduction for geometers, Ann. Univ. Ferrara 61 (2015), 65–117. https://doi.org/10.1007/s11565-014-0202-7
• M.-W. Cheung, C. Ikenmeyer and S. Mkrtchyan, Symmetrizing tableaux and the 5th case of the Foulkes conjecture, J. Symbolic Comput. 80 (2017), 833–843. https://doi.org/10.1016/j.jsc.2016.09.002
• C. Raicu, S. V. Sam and J. Weyman, On some modules supported in the Chow variety, Vietnam J. Math. 50 (2022), 501–521. https://doi.org/10.1007/s10013-021-00527-2
• OpenAI, Quadratic stabilization of the canonical Foulkes–Howe map, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quadratic-Stabilization-of-the-Canonical-Foulkes-Howe-Map-September-25-2026/paper.pdf

Motivation: when does a split tangent bundle come from a product?

If a complex manifold is a product $Y_1\times Y_2$, its holomorphic tangent bundle is the direct sum of the tangent bundles of the factors. The converse question asks when a given holomorphic decomposition $T_X=E_1\oplus E_2$ of the tangent bundle of a compact manifold $X$ comes from a product decomposition of its universal cover, with the product realizing the specified summands rather than some other splitting. This is the complex-analytic counterpart of the de Rham decomposition theorem for Riemannian manifolds with parallel complementary distributions (de Rham 1952), but a holomorphic splitting supplies no complete metric making the distributions parallel, so de Rham's argument does not apply. The question sits between foliation theory, Kähler geometry and the classification of projective manifolds with split tangent bundle.

Timeline

• 1952 — de Rham: a complete Riemannian manifold with parallel complementary orthogonal distributions has universal cover isometric to a product (de Rham 1952).
• 1993 — Yau proves a splitting theorem for Kähler–Einstein manifolds (Yau, Comm. Anal. Geom. 1 (1993)).
• 2000 — Beauville formulates the compatible universal-cover conjecture for compact Kähler manifolds whose tangent summands have integrable partial sums, and proves it for Kähler–Einstein manifolds and compact Kähler surfaces (Beauville 2000, Section 2.3, Theorems A and C). Druel treats projective manifolds whose tangent bundle is a sum of line bundles (Druel 2000).
• 2006 — Brunella, Pereira and Touzet settle the case of a line summand with integrable complement on compact Kähler manifolds (BPT 2006).
• 2007 — Höring proves automatic integrability for split tangent bundles on non-uniruled projective manifolds (Höring 2007).
• 2013–2024 — Pereira–Touzet obtain a compatible Euclidean factor when one involutive summand is Hermitian flat (PT 2013); Druel, Pereira, Pym and Touzet handle a foliation with a compact leaf with finite holonomy (DPPT 2022) and numerically flat regular foliations (DPPT 2024).
• 2026 — Höring proves algebraic integrability for tangent summands on klt Fano-type varieties (Höring 2026). An OpenAI preprint, Universal-cover splitting for compact Kähler manifolds (OpenAI Math Release, September 23, 2026), claims the two-summand case of Beauville's conjecture in arbitrary positive ranks. 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 holomorphic charts to $\mathbb C^n$. A Kähler metric is a smooth Riemannian metric $g$ on the real tangent bundle that is Hermitian ($g(Ju,Jv)=g(u,v)$ for multiplication $J$ by $i$) and whose fundamental form $\omega(u,v)=g(Ju,v)$ is closed.

A holomorphic splitting of $T_X$ with ranks $r_1,r_2$ is given by a field $P$ of $\mathbb C$-linear idempotents $P_x:T_xX\to T_xX$, holomorphic in charts, with $\operatorname{rank}P_x=r_1$ and $\dim\ker P_x=r_2$; then $E_1=\operatorname{im}P$, $E_2=\ker P$ and $T_X=E_1\oplus E_2$. A subbundle is integrable if its local holomorphic sections are closed under the Lie bracket. The ordinary universal cover $\pi:\widetilde X\to X$ is a connected, simply connected covering space carrying the lifted complex structure.

Formalization targets

Goal: Theorem 1.1 (compatible universal-cover splitting)

Let $X$ be a compact connected Kähler manifold of complex dimension $n\ge2$ and $T_X=E_1\oplus E_2$ a holomorphic splitting into integrable subbundles of positive ranks $r_1,r_2$. Then there are connected, simply connected complex manifolds $Y_1,Y_2$ with $\dim_{\mathbb C}Y_i=r_i$ and a biholomorphism $\Phi:\widetilde X\to Y_1\times Y_2$ with

$$d\Phi\big(\pi^*E_1\big)=\mathrm{pr}_1^*T_{Y_1},\qquad d\Phi\big(\pi^*E_2\big)=\mathrm{pr}_2^*T_{Y_2}.$$

The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem proves the two-summand form of Beauville's conjecture with no flatness, compact-leaf or line-bundle assumption: integrability of both summands and a Kähler metric on a compact manifold suffice. Combined with Höring's integrability theorem it gives compatible product decompositions for every split tangent bundle on a non-uniruled projective manifold (Corollary 1.2), and for projective manifolds with nef and big canonical bundle (Corollary 1.3). With the companion preprint on rationally connected manifolds it also covers split tangent bundles there. The factors may be noncompact, and the conclusion concerns the universal cover, not a finite cover.

Formalizing it. The statement involves universal covers, Kähler forms, holomorphic distributions and biholomorphisms of products, all of which must be expressed with Mathlib's manifold library. A machine-checked proof would certify a global continuation argument (Hartogs-type extension, boundary crossing, path rectangles and monodromy) for which no prior formal treatment exists.

Difficulty

Integrability alone gives, by holomorphic Frobenius, local product coordinates. The obvious strategy is to continue these local products along paths and use simple connectivity of $\widetilde X$. This fails because a path in one foliation need not be transportable along a path in the other: local product charts can break down, and leaves can be noncompact and dense. Compactness makes every metric complete, but does not make the foliations parallel, so the de Rham argument is unavailable. Beauville's example on $A\times\mathbb P^1$ ($A$ an abelian surface) shows that even when $X$ is a product, a non-integrable complementary summand need not be realized by any product structure, so both integrability hypotheses are needed.

Formalization scope

• ComplexManifold n bundles a Hausdorff, second-countable type with an atlas modeled on Fin n → ℂ that is smooth for 𝓘(ℂ, Fin n → ℂ), i.e. holomorphic transition maps.
• KahlerMetric X is a real bilinear form on each tangent space that is symmetric, positive definite, invariant under multiplication by Complex.I, smooth in every chart, and whose fundamental form is closed (the cyclic sum of its chart derivatives vanishes).
• HolomorphicSplitting X r₁ r₂ is a field of idempotent continuous ℂ-linear maps, holomorphic in charts, with range of rank $r_1$ and kernel of rank $r_2$. Integrable P says that chart-local holomorphic vector fields with values in the range of $P$ have bracket in the range of $P$; both S.projection and the complementary projection are assumed integrable.
• OrdinaryUniversalCover X Z is a covering map from a connected, simply connected complex manifold $Z$ that is a local biholomorphism.
• CompatibleProduct asks for a homeomorphism $\Phi:Z\to Y_1\times Y_2$, holomorphic with holomorphic inverse, whose differential sends the pullback of $E_1$ onto $\ker(\mathrm{snd})$ and the pullback of $E_2$ onto $\ker(\mathrm{fst})$.
• Hypotheses: $X$ compact and connected, $n\ge2$, $r_1,r_2>0$. A rank-zero summand would make the statement trivial and is excluded, as in the source.
• Infrastructure needed: holomorphic Frobenius, foliation leaves, meromorphic Hartogs extension, Stokes' theorem for Kähler forms, monodromy for covering spaces. The Kähler-metric and splitting definitions are reusable for the companion integrability mission.

Selected references

• G. de Rham, Sur la réductibilité d'un espace de Riemann, Comment. Math. Helv. 26 (1952), 328–344. https://doi.org/10.1007/BF02564308
• S.-T. Yau, A splitting theorem and an algebraic geometric characterization of locally Hermitian symmetric spaces, Comm. Anal. Geom. 1 (1993), 473–486.
• A. Beauville, Complex manifolds with split tangent bundle, in Complex Analysis and Algebraic Geometry (de Gruyter, 2000), 61–70. https://doi.org/10.1515/9783110806090-004
• S. Druel, Variétés algébriques dont le fibré tangent est totalement décomposé, J. Reine Angew. Math. 522 (2000), 161–171. https://arxiv.org/abs/math/9901138v2
• M. Brunella, J. V. Pereira, F. Touzet, Kähler manifolds with split tangent bundle, Bull. Soc. Math. France 134 (2006), 241–252. https://doi.org/10.24033/bsmf.2507
• A. Höring, Uniruled varieties with split tangent bundle, Math. Z. 256 (2007), 465–479. https://doi.org/10.1007/s00209-006-0072-5
• J. V. Pereira, F. Touzet, Foliations with vanishing Chern classes, Bull. Braz. Math. Soc. 44 (2013), 731–754. https://arxiv.org/abs/1210.5916v1
• S. Druel, J. V. Pereira, B. Pym, F. Touzet, A global Weinstein splitting theorem for holomorphic Poisson manifolds, Geom. Topol. 26 (2022), 2831–2853. https://doi.org/10.2140/gt.2022.26.2831
• S. Druel, J. V. Pereira, B. Pym, F. Touzet, Numerically flat foliations and holomorphic Poisson geometry, preprint (2024). https://arxiv.org/abs/2411.08806v1
• A. Höring, Fano varieties with split tangent sheaf, preprint (2026). https://arxiv.org/abs/2602.15427v1
• OpenAI, Universal-cover splitting for compact Kähler manifolds, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 3). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-cover-splitting-for-compact-Kahler-manifolds-September-23-2026/paper.pdf

Motivation

Zariski's cancellation problem asks whether affine space can be recognized from its cylinder: if a variety $X$ satisfies $X\times\mathbb A^1\cong\mathbb A^{n+1}$, must $X\cong\mathbb A^n$? Algebraically, for a finitely generated commutative $\mathbb C$-algebra $A$ and an independent variable $w$,

$$A[w]\cong\mathbb C^{[n+1]}\ \overset{?}{\Longrightarrow}\ A\cong\mathbb C^{[n]},$$

where $\mathbb C^{[r]}$ is a polynomial ring in $r$ variables and all isomorphisms are $\mathbb C$-algebra isomorphisms. The problem is one of the central questions of affine algebraic geometry, closely tied to the recognition of affine space, coordinates of polynomial rings, and polynomial fibrations.

Background

• 1972. Abhyankar, Heinzer and Eakin prove cancellation for the affine line (doi:10.1016/0021-8693(72)90134-2).
• 1974. Dolgachev and Weisfeiler formulate the affine-fibration conjecture (doi:10.1070/IM1974v008n04ABEH002127).
• 1979–1980. Fujita, and Miyanishi and Sugie, prove cancellation for the complex affine plane (doi:10.3792/pjaa.55.106, doi:10.1215/kjm/1250522319).
• 1987. Asanuma constructs, in positive characteristic, threefolds whose cylinders are affine four-space (doi:10.1007/BF01389155).
• 1996. Makar-Limanov uses additive group actions to show that the Russell cubic is not $\mathbb C^3$ (doi:10.1007/BF02937314).
• 2014. Gupta proves failure of cancellation in every dimension $\ge3$ over every field of positive characteristic (doi:10.1007/s00222-013-0455-2, doi:10.1016/j.aim.2014.07.012).
• 2018–2021. El Kahoui–Ouali and Dutta–Lahiri prove that residual coordinates are one-stably coordinates (doi:10.1216/JCA-2018-10-3-317, doi:10.1016/j.jpaa.2021.106707).
• 2026. Gaifullin and Petrov still list the characteristic-zero problem in dimension $\ge3$ as unresolved (arXiv:2607.13593).

The source of this mission is an OpenAI preprint dated September 23, 2026.

Setting

Let $p,s,u,F,J$ be independent variables over $\mathbb C$ and $P=\mathbb C[p,s,u,F,J]$. Put

$$x=s^2+u^3+p^2F,\qquad H=x^2F-(1+2sx)J-p^2J^2-pu,\qquad A=P/(H).$$

So $A$ is the coordinate ring of the hypersurface $\{H=0\}\subset\mathbb A^5$. For a $\mathbb C$-algebra $A$, $A[w]$ denotes the polynomial ring in one further variable, and $\mathbb C^{[r]}$ the polynomial ring in $r$ variables.

Formalization targets

Goal: Theorem 1.1

$$A\ \text{is a finitely generated integral domain of Krull dimension }4,\qquad A[w]\cong_{\mathbb C}\mathbb C^{[5]},\qquad A\not\cong_{\mathbb C}\mathbb C^{[4]}.$$

The Lean statement OAI.ComplexCancellation.main is open on the platform.

Significance

Theorem 1.1 gives a negative answer to Zariski's cancellation problem over $\mathbb C$ in dimension four, with an explicit counterexample of degree small enough to write in one line. The same polynomial yields two further consequences proved in the paper: $H$ is a coordinate of $P[w]$ but not of $P$, so the Stable Coordinate Conjecture fails in ambient dimension five (Corollary 1.2); and the maps $p:\operatorname{Spec}A\to\mathbb A^1$ and $(p,H):\mathbb A^5\to\mathbb A^2$ are smooth $\mathbb A^3$-fibrations that are not Zariski-locally trivial, disproving the Dolgachev–Weisfeiler conjecture over these bases (Corollary 7.1). Cancellation in dimension three over $\mathbb C$ is not addressed.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

The cylinder isomorphism $A[w]\cong\mathbb C^{[5]}$ is comparatively explicit: a locally nilpotent derivation sends $H$ to $p^3$, and exponentiating converts $H$ into $H+p^3w$. The hard part is proving $A\not\cong\mathbb C^{[4]}$. Standard invariants do not help: $A$ is smooth, factorial-type obstructions vanish, and topologically $\operatorname{Spec}A$ is contractible like $\mathbb C^4$ since its cylinder is $\mathbb C^5$. The paper uses additive group actions (locally nilpotent derivations), passing to an associated graded algebra along $p=0$, lifting actions through a line bundle over a smooth affine quadric, and a rigidity argument based on the Mason–Stothers polynomial abc inequality.

Formalization scope

• P := MvPolynomial (Fin 5) ℂ with p, s, u, F, J := X 0, …, X 4; x and H are transcribed literally; A := P ⧸ Ideal.span {H}.
• Dimension is ringKrullDim A = 4; integrality is IsDomain A; finite generation is Algebra.FiniteType ℂ A.
• The cylinder statement is Nonempty (Polynomial A ≃ₐ[ℂ] MvPolynomial (Fin 5) ℂ); the non-polynomiality is ¬ Nonempty (A ≃ₐ[ℂ] MvPolynomial (Fin 4) ℂ). All isomorphisms are $\mathbb C$-algebra isomorphisms.

A complete development needs: explicit polynomial automorphisms (for the cylinder), Krull dimension of hypersurface quotients, locally nilpotent derivations and their kernels, filtrations and associated graded rings, and the Mason–Stothers theorem for polynomials. Contributions formalizing Proposition 2.2, Proposition 3.4 (the graded identification), Propositions 4.1–4.3, Lemma 5.1 (order of a locally nilpotent derivation), Lemma 6.1 (Mason–Stothers) and Proposition 6.3 are welcome.

Selected references

• OpenAI, An explicit failure of complex affine-space cancellation, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026/paper.pdf
• N. Gupta, On Zariski's cancellation problem in positive characteristic, Adv. Math., 2014. https://doi.org/10.1016/j.aim.2014.07.012
• N. Gupta, On the cancellation problem for the affine space $\mathbb A^3$ in characteristic $p$, Invent. Math., 2014. https://doi.org/10.1007/s00222-013-0455-2
• S. S. Abhyankar, W. Heinzer, P. Eakin, On the uniqueness of the coefficient ring in a polynomial ring, J. Algebra, 1972. https://doi.org/10.1016/0021-8693(72)90134-2
• T. Fujita, On Zariski problem, Proc. Japan Acad. Ser. A, 1979. https://doi.org/10.3792/pjaa.55.106
• L. Makar-Limanov, On the hypersurface $x+x^2y+z^2+t^3=0$ in $\mathbb C^4$ or a $\mathbb C^3$-like threefold which is not $\mathbb C^3$, Israel J. Math., 1996. https://doi.org/10.1007/BF02937314
• A. K. Dutta, A. Lahiri, On residual and stable coordinates, J. Pure Appl. Algebra, 2021. https://doi.org/10.1016/j.jpaa.2021.106707
• M. El Kahoui, M. Ouali, A note on residual coordinates of polynomial rings, J. Commut. Algebra, 2018. https://doi.org/10.1216/JCA-2018-10-3-317
• B. Yu. Weisfeiler, I. V. Dolgachev, Unipotent group schemes over integral rings, Math. USSR-Izv., 1974. https://doi.org/10.1070/IM1974v008n04ABEH002127
• S. Gaifullin, M. Petrov, Non-cancellative varieties, maximal tori, and the Makar-Limanov invariant, preprint, 2026. https://arxiv.org/abs/2607.13593

Motivation: curvature of the central path as a complexity measure

Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:

• 2005. Dedieu and Shub conjecture that the total curvature of the central path is bounded linearly in the dimension. Dedieu, Malajovich and Shub prove an $O(n)$ bound on average over the regions of a hyperplane arrangement. De Loera, Sturmfels and Vinzant later obtain the same averaged bound with matroid methods (arXiv:1012.3978).
• 2008–2009. Deza, Terlaky and Zinchenko build redundant Klee–Minty cubes and "snakes" with curvature $\Omega(m)$ for $m$ inequalities, which refutes the dimension version. They then conjecture the continuous analogue of the Hirsch conjecture: the total curvature is bounded linearly in the number of constraints.
• 2014–2017. Allamigeon, Benchimol, Gaubert and Joswig disprove that conjecture with a family of linear programs whose central paths have curvature exponential in the number of constraints. The bound first appeared in arXiv:1405.4161 and was given an elementary tropical proof in arXiv:1708.01544v2, Theorem 25, which is the result of this mission.

Setting

A linear program in slack form has a real $m\times n$ matrix $A$, $b\in\mathbb R^m$, $c\in\mathbb R^n$ and $N:=n+m$:

$$\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. } Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .$$

For $\mu>0$ the point of the central path $(x^\mu,w^\mu,s^\mu,y^\mu)\in\mathbb R^{2N}$ is the unique solution of

$$Ax+w=b,\quad s-A^\top y=c,\quad x_js_j=\mu,\quad w_iy_i=\mu,\quad x,w,s,y>0. \tag{1}$$

The primal central path is $\mu\mapsto(x^\mu,w^\mu)\in\mathbb R^N$.

For $r\ge1$ and $t>0$, the program $\mathbf{LW}_r(t)$ minimizes $x_1$ over $x\in\mathbb R^{2r}$ subject to

$$x_1\le t^2,\quad x_2\le t,\quad x_{2j+1}\le t\,x_{2j-1},\quad x_{2j+1}\le t\,x_{2j},\quad x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ \ (1\le j<r),\quad x\ge0 .$$

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$, $m=3r-1$, $N=5r-1$.

For points $U,V,W$ of Euclidean space with $U\ne V\ne W$, the turning angle $\angle UVW\in[0,\pi]$ is the angle between the vectors $V-U$ and $W-V$. For a curve $\sigma$ parameterized over $I\subseteq\mathbb R$, the total curvature is

$$\kappa(\sigma,I)=\sup\Big\{\sum_{k=1}^{p-1}\angle\,\sigma(\mu_{k-1})\sigma(\mu_k)\sigma(\mu_{k+1})\ :\ \mu_0<\dots<\mu_p\ \text{in } I\Big\}\in[0,+\infty].$$

The milestones also use the field $\mathbb K$ of absolutely convergent generalized real Puiseux series $\sum_{\alpha\in\mathbb R}a_\alpha t^\alpha$. Such a series can be evaluated at large real $t$, and it has a valuation $\mathrm{val}\in\mathbb T=\mathbb R\cup\{-\infty\}$, its leading exponent. Read over $\mathbb K$, $\mathbf{LW}_r$ is one linear program. The valuation of its central path at $\mu=t^\lambda$ is the tropical central path $\mathcal C^{\mathrm{trop}}(\lambda)\in\mathbb R^{2N}$, a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).

Formalization targets

Goal: Theorem 25

For every $r\ge1$ and $\epsilon>0$ there is $t_0$ such that for all $t>t_0$,

$$\kappa\big(\mu\mapsto(x^\mu,w^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon\quad\text{and}\quad\kappa\big(\mu\mapsto(x^\mu,w^\mu,s^\mu,y^\mu),(0,\infty)\big)>\big(2^{r-2}-1\big)\tfrac\pi2-\epsilon$$

for the central path of $\mathbf{LW}^=_r(t)$. Here $t_0$ may depend on $r$ and $\epsilon$. Both the primal and the primal-dual curves are part of the goal, as in the paper.

Milestones, in the order of the paper's argument

1. Lemma 22: for non-null $\mathbf x,\mathbf y\in\mathbb K^d$, the angle $\angle\mathbf x(t)\mathbf y(t)$ has a limit, which is $\pi/2$ when the arg maxes of $\mathrm{val}\,\mathbf x$ and $\mathrm{val}\,\mathbf y$ are disjoint.
2. Lemma 23: the turning angle $\angle\mathbf U(t)\mathbf V(t)\mathbf W(t)\to\pi/2$ when $\max\mathrm{val}\,\mathbf U<\max\mathrm{val}\,\mathbf V<\max\mathrm{val}\,\mathbf W$ and the arg maxes of $\mathrm{val}\,\mathbf V$ and $\mathrm{val}\,\mathbf W$ are disjoint.
3. Proposition 24: $\liminf_{t}\kappa(\mathcal C_t,[t^{\lambda_0},t^{\lambda_p}])\ge\sum_{k=1}^{p-1}\angle^*\mathcal C^{\mathrm{trop}}(\lambda_{k-1})\mathcal C^{\mathrm{trop}}(\lambda_k)\mathcal C^{\mathrm{trop}}(\lambda_{k+1})$, where $\angle^*$ is the weak tropical angle ($\pi/2$ under the conditions of Lemma 23, else $0$).
4. Table 1: the coordinates of the tropical central path of $\mathbf{LW}_r$ at $\lambda=(4k+2c)/2^j$.
5. Claims in the proof of Theorem 25 (p. 23): on $[0,2]$ the dual coordinates of $\mathcal C^{\mathrm{trop}}$ are at most $\max(0,\lambda-1)$. At $\lambda_k=4k/2^{r-1}$ the largest coordinate is $r-1+(2k+2)/2^{r-1}$, attained only by $w_{3(r-1)}$ or $w_{3(r-1)+1}$. Hence $\angle^*=\pi/2$ at each interior subdivision point.

Significance

The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: $\mathbf{LW}_r$ has $3r+1$ constraints and curvature at least about $2^{r-2}\pi/2$. This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.

The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.

Difficulty

The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large $t$. The central path of $\mathbf{LW}^=_r(t)$ has no closed form, so its points cannot be written down at given parameters $\mu$. Numerical evidence at a fixed $t$ says nothing uniform in $r$. The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with $r$. What is needed is control of the path's geometry uniformly over the whole scale of $t$, with $2^{r-2}$ turns located at once, and the threshold $t_0$ is not explicit.

Formalization scope

Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is $\pi$ minus it. A degenerate triple ($U=V$ or $V=W$) contributes angle $0$. Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set $(0,\infty)$. The primal and primal-dual curves are the vectors $(x,w)\in\mathbb R^{5r-1}$ and $(x,w,s,y)\in\mathbb R^{2(5r-1)}$. System (1) is the published Vanderbei central-path system with objective $-c$. The goal quantifies over every curve solving (1) for all $\mu>0$. Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers $2^{r-2}$ use integer exponents of the real number $2$.

A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be $0$), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.

Lemmas 22–24 are stated over a model of $\mathbb K$ by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in $\mathbb K$ are expressed through evaluation at all sufficiently large $t$, which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of $\mathbf{LW}_r$ given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at $r=2$, $k=0$, where $w_1=w_4=2$. It is stated with that case excluded, which the proof does not use.

Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over $\mathbb K$ and its real specializations.

Selected references

• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-Barrier Interior Point Methods Are Not Strongly Polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; preprint v2 (cited throughout) arXiv:1708.01544, doi:10.1137/17M1142132.
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Long and winding central paths, preprint, 2014. arXiv:1405.4161
• J. A. De Loera, B. Sturmfels, C. Vinzant, The central curve in linear programming, Found. Comput. Math. 12(4), 2012. arXiv:1012.3978
• J.-P. Dedieu, G. Malajovich, M. Shub, On the curvature of the central path of linear programming theory, Found. Comput. Math. 5(2), 2005.
• J.-P. Dedieu, M. Shub, Newton flow and interior point methods in linear programming, Int. J. Bifurcation and Chaos 15(3), 2005.
• A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Springer, 2009.
• L. van den Dries, P. Speissegger, The real field with convergent generalized power series, Trans. Amer. Math. Soc. 350(11), 1998.

Motivation

Interior point methods solve linear programs in a number of arithmetic operations polynomial in the bit length of the input (Karmarkar 1984). Whether linear programming admits a strongly polynomial algorithm, one whose number of arithmetic operations is bounded by a polynomial in the number of variables and constraints alone, is open; it is the ninth of Smale's problems for the next century (Smale 1998/2000, see the references). A natural question is whether some interior point method is strongly polynomial. Primal-dual path-following methods follow the central path of a log-barrier problem and are the methods used in practice.

Allamigeon, Benchimol, Gaubert and Joswig (arXiv:1708.01544, SIAM J. Appl. Algebra Geom. 2018) gave such a family. For linear programs $\mathbf{LW}_r(t)$ with $2r$ variables and $3r+1$ constraints, every path-following method that stays in the wide neighborhood of the central path needs at least $2^{r-1}$ iterations once $t$ is large enough. The same family disproves the "continuous Hirsch conjecture" of Deza, Terlaky and Zinchenko (DTZ09, see the references) on the total curvature of the central path. That curvature result is the subject of a separate mission. This mission formalizes the iteration bound.

Setting

For a real $m\times n$ matrix $A$, $b\in\mathbb R^m$, $c\in\mathbb R^n$ and $N:=n+m$, the paper considers the linear program in slack form and its dual,

$$\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. }\ Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .$$

A primal-dual point is $z=(x,w,s,y)\in\mathbb R^{2N}$. The set $\mathcal F^\circ$ of strictly feasible points consists of the $z$ with all $2N$ coordinates positive that satisfy both equality systems. The duality measure is

$$\bar\mu(z)=\frac1N\big(\langle x,s\rangle+\langle w,y\rangle\big),$$

and for $0<\theta<1$ the wide neighborhood of the central path is

$$\mathcal N^{-\infty}_\theta=\Big\{z\in\mathcal F^\circ:\ x_js_j\ge(1-\theta)\bar\mu(z)\ \forall j,\ \ w_iy_i\ge(1-\theta)\bar\mu(z)\ \forall i\Big\}.$$

The central path itself is the set of points where all products $x_js_j$, $w_iy_i$ are equal. The neighborhood bounds the products only from below. It contains the $\ell_2$ and $\ell_\infty$ neighborhoods used by short-step, long-step and predictor-corrector methods.

The instance is $\mathbf{LW}_r(t)$, for $r\ge1$ and $t>0$:

$$\min\ x_1\ \text{ s.t. }\ x_1\le t^2,\ x_2\le t,\ x_{2j+1}\le t\,x_{2j-1},\ x_{2j+1}\le t\,x_{2j},\ x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ (1\le j<r),\ x_{2r-1},x_{2r}\ge0 .$$

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$, $m=3r-1$, $N=5r-1$. Its wide neighborhood is written $\mathcal N^{-\infty}_{\theta,t}$. A polygonal curve is a union $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ of $p$ segments, and it is contained in the neighborhood when every point of every segment is.

The milestones use the tropical semifield $\mathbb T=\mathbb R\cup\{-\infty\}$ with $a\oplus b=\max(a,b)$ and $a\odot b=a+b$. The tropical segment $\mathsf{tsegm}(u,v)$ is the set of points $\lambda\odot u\oplus\mu\odot v$ with $\lambda\oplus\mu=0$. The Funk metric is $\delta_F(x,y)=\max(0,\max_k(y_k-x_k))$, with $d_\infty(x,y)=\max(\delta_F(x,y),\delta_F(y,x))$ and the directed Hausdorff distance $d_\infty(X,Y)=\sup_{x\in X}\inf_{y\in Y}d_\infty(x,y)$. Finally, $\log_t$ is applied coordinatewise, with $\log_t0=-\infty$.

Formalization targets

Goal: Theorem 30 (p. 27)

Let $r\ge1$ and $0<\theta<1$, and suppose that

$$t>\Big(\max\Big((10r-2)!,\ \frac{((10r-1)!)^{24}}{(1-\theta)^3}\Big)\Big)^{2^{r-1}} .\tag{36}$$

If a polygonal curve $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ is contained in $\mathcal N^{-\infty}_{\theta,t}$ with $\bar\mu(z^0)\le1$ and $\bar\mu(z^p)\ge t^2$, then

$$p\ge2^{r-1}.$$

The threshold (36) is the paper's own explicit constant. Corollary 31 (Theorem B of the introduction) restates the result for algorithms. Any method whose iterates and the segments joining them stay in the wide neighborhood performs at least $2^{r-1}$ iterations to reduce the duality measure from $t^2$ to $1$.

Milestones

1. Proposition 1 (p. 5). On the primal-dual feasible set, $\bar\mu((1-\alpha)z+\alpha z')=(1-\alpha)\bar\mu(z)+\alpha\bar\mu(z')$ for all $\alpha\in\mathbb R$.
2. Lemma 5 (p. 10). For $u\le v$ in $\mathbb T^d$, $\mathsf{tsegm}(u,v)$ is a polygonal curve whose segments, oriented from $u$ to $v$, have directions $e^{K_1},\dots,e^{K_\ell}$ with $K_1\subsetneq\dots\subsetneq K_\ell$ and $\ell\le d$.
3. Lemma 8 (p. 11). For a segment $S=[u,v]$ in $\mathbb R^d_+$ and $t>1$,

$$d_\infty\big(\mathsf{tsegm}(\log_tu,\log_tv),\ \log_tS\big)\le\log_t2 .$$

4. Lemma 11 (p. 13). For a $d\times d$ matrix $\mathbf M$ with monomial entries $\pm t^{\alpha_{ij}}$ and $t>1$, $\log_t|\det\mathbf M(t)|$ and $\operatorname{val}(\det\mathbf M)$ differ by at most $\log_td!$; the lower bound holds once $t\ge(d!)^{1/\eta(\mathbf M)}$.
5. Proposition 20 (p. 19). The explicit recursion for $x^\lambda$ gives the greatest point of the tropical polyhedron $\{x\in\mathcal P':x_1\le\lambda\}$, where $\mathcal P'\subseteq\mathbb T^{2r}$ is cut out by the tropicalized constraints (26) of $\mathbf{LW}_r$.

Significance

The theorem shows that the iteration count of a large class of primal-dual log-barrier interior point methods cannot be bounded by any function of $r$ that grows more slowly than $2^{r-1}$, uniformly in the data. The class includes the methods of Kojima–Mizuno–Yoshise, Monteiro–Adler and Mizuno–Todd–Ye. No such method is strongly polynomial. The constraint matrix of $\mathbf{LW}_r(t)$ is fixed by $r$ and $t$ alone, so the bound concerns the combinatorial dimension, not the bit length. The only property of the method used is that its trajectory stays in $\mathcal N^{-\infty}_{\theta,t}$. The lower bound therefore applies to every method with that property, whatever rule chooses its steps.

The result is proved in the paper; no machine-checked proof of it or of its tropical ingredients is known. A formalization would check the explicit threshold (36), which the paper derives in a few lines from bounds on Puiseux polyhedra. It would also produce reusable statements about tropical segments, the Funk and Hilbert metrics on $\mathbb T^d$, and determinants of monomial matrices.

Difficulty

Following the central path is not hard in principle: the obvious argument tracks the duality measure, which decreases by a constant factor per iteration in a neighborhood of the path. That argument gives only upper bounds. The lower bound requires showing that the neighborhood itself, for large $t$, is too thin to be crossed in a few straight steps, uniformly over every possible trajectory. The paper does this by passing to the limit $t\to\infty$ on logarithmic scale. The image of $\mathcal N^{-\infty}_{\theta,t}$ under $\log_t$ collapses onto a piecewise-linear tropical central path, and a segment of $\mathbb R^{2N}$ becomes, up to $\log_t2$, a tropical segment. The tropical central path of $\mathbf{LW}_r$ then has to be shown to need $2^{r-1}$ tropical segments. The limit argument has to be made quantitative at a finite, explicit $t$. That is where the Puiseux-series machinery (Theorems 12, 15 and 19 of the paper) and the explicit constant enter.

Formalization scope

Everything is stated over $\mathbb R$ and $\mathbb T$; the goal typechecks without the field of Puiseux series. A primal-dual point is an element of $\mathbb R^n\times\mathbb R^m\times\mathbb R^n\times\mathbb R^m$. The dual equation is $s-A^\top y=c$ with Mathlib's transpose, $\bar\mu$ divides by $N=n+m$ (equal to $5r-1$ for $\mathbf{LW}^=_r$), and the wide neighborhood is one-sided. The instance matrix is generated from the paper's 1-based row and column numbers; Lean indices are 0-based. A polygonal curve is a map $z:\{0,\dots,p\}\to\mathbb R^{2N}$ with segment ℝ (z i) (z (i+1)) ⊆ N. The power $2^{r-1}$ in (36) is a natural-number power and the factorials are natural-number factorials. $\mathbb T$ is WithBot ℝ, and distances that can be infinite take values in EReal, with the convention $-\infty+(+\infty)=-\infty$ encoded explicitly.

Two statements are repaired or restated. Lemma 11 is printed for all $t>0$, but its first inequality fails for $0<t<1$ (for $\mathbf M=\begin{pmatrix}t&1\\1&1\end{pmatrix}$ at $t=1/2$), so it is stated for $t>1$. Lemma 8 makes explicit its implicit hypotheses $t>1$ and $u,v\ge0$. Proposition 20 is stated in the form its proof establishes, as the greatest point of a tropical polyhedron. Its identification with the valuation of the Puiseux central path is not part of the item. Monomial matrices are given by sign and exponent matrices, and the valuation of the determinant is computed from the permutation expansion.

A trivializing formalization is ruled out: $\mathcal N^{-\infty}_{\theta,t}$ is not empty, since the build includes a sorry-free proof that it contains an explicit point for $r=1$, $t=2$, $\theta=1/2$. A curve with $p=0$ cannot satisfy both duality-measure conditions, since $t^2>1$.

The paper's Puiseux-series results are not posed: Theorems 12, 15, 19 and 29, Propositions 14, 16, 21 and 28, Corollary 17, and the count $\gamma([0,2])\ge2^{r-1}$ of §6.2. They need a faithful model of the field of absolutely convergent generalized Puiseux series and of the tropical central path. Contributions of that infrastructure, and of these statements as further milestones, are welcome. So are proofs of the five milestones, which need no Puiseux series. Proposition 1, Lemma 5 and Proposition 20 are elementary, and Lemma 8 and Lemma 11 are estimates with explicit constants.

Selected references

• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; arXiv:1708.01544v2. https://arxiv.org/abs/1708.01544
• A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Adv. Mech. Math. 17, Springer, 2009, pp. 223–256. https://doi.org/10.1007/978-0-387-75714-8
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2), 1998, 7–15; reprinted in Mathematics: Frontiers and Perspectives, AMS, 2000. https://doi.org/10.1007/BF03025291
• M. Develin, B. Sturmfels, Tropical convexity, Doc. Math. 9, 2004. https://arxiv.org/abs/math/0308254
• S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453
• X. Allamigeon, S. Gaubert, M. Skomra, Tropical spectrahedra, Discrete Comput. Geom. 63, 2020; arXiv:1610.06746. https://arxiv.org/abs/1610.06746