View source for Anticanonical nonvanishing under smooth semipositivity

'''Anticanonical nonvanishing''' asks whether a smooth complex projective variety whose anticanonical bundle is semipositive has a nonzero section of some positive power of that bundle. Yau listed a version of the question in his 1994 problem list. Seven manuscripts in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), dated 26 September 2026, claim an affirmative answer when the anticanonical bundle carries a smooth Hermitian metric of semipositive curvature, in every dimension. This page summarizes the published claims and lists publicly available follow-up work.

== Background ==
* As recounted in the introduction of the main manuscript:
** ''The question.'' For a smooth projective complex variety ''X'', a smooth Hermitian metric of semipositive curvature on −''K''<sub>''X''</sub> makes the anticanonical class nef. The nonvanishing question asks whether ''H''<sup>0</sup> of −''mK''<sub>''X''</sub> is nonzero for some integer ''m'' &gt; 0. The manuscript calls this the positive-multiple formulation associated with Yau's question, Problem 75 of his 1994 list. It notes, with the example of an Enriques surface times the projective line, that a positive multiple can be needed even when −''K''<sub>''X''</sub> is not torsion.
** ''Structure theory.'' Yau's prescribed-Ricci theorem of 1978 realizes the given semipositive anticanonical curvature as the Ricci form of a Kähler metric. The structure results of Demailly–Peternell–Schneider (1996) and Campana–Demailly–Peternell (2015) then describe the universal cover by flat, compact Ricci-flat and remaining compact factors.
** ''The nef setting.'' Lazić, Matsumura, Peternell, Tsakanikas and Xie proved numerical effectivity for log canonical threefold pairs with nef log-anticanonical divisor, under further hypotheses on the singularities, in [https://arxiv.org/abs/2202.13814 arXiv:2202.13814], and Müller proved nonvanishing for klt pairs in dimension three and under a semiampleness hypothesis in general.

== The original results ==
* '''Anticanonical nonvanishing (26 September 2026).''' Theorem 1.1 of the main manuscript states: let ''X'' be a smooth connected projective variety over the complex numbers; if −''K''<sub>''X''</sub> admits a smooth Hermitian metric of semipositive curvature, then ''H''<sup>0</sup> of −''mK''<sub>''X''</sub> is nonzero for some integer ''m'' &gt; 0.
** ''Method, as described:'' after Yau's theorem and the structure theory, the flat and Ricci-flat factors of the universal cover supply canonical frames. On the remaining factor, a projective variety without holomorphic forms of positive degree, the deck transformations act through a compact torus, and the manuscripts construct an anticanonical section fixed by that torus. Its product with the frames descends to a finite étale cover, and its norm gives a section on ''X''.
** The six companion manuscripts treat the torus-equivariant steps: invariant Euler characteristics and twisted differentials, bounded anticanonical metrics on klt pairs and torus quotients, cohomological transfer, metric descent, integrable metrics with controlled boundary, and exact orders of invariant anticanonical linear systems.
* '''Sources.''' Commit <code>1581d4c</code> of the openai/math repository, folder [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Anticanonical-nonvanishing-from-smooth-semipositivity-September-26-2026 Anticanonical nonvanishing from smooth semipositivity] for the main manuscript; the six companions are listed in the collection's contents file under family 068.
* '''Formalization.''' The collection has no Lean scope note (<code>lean/docs/</code>) or Comparator challenge for this family.
** The repository's Lean library contains a theorem <code>prescribedRicciFromSemipositive</code> in [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/OAI/Geometry/PrescribedRicci/PrescribedRicci.lean lean/OAI/Geometry/PrescribedRicci/PrescribedRicci.lean]. It concerns a compact connected Hausdorff space with a finite holomorphic atlas, a holomorphic projective embedding and a smooth semipositive metric on the anticanonical bundle. Its conclusion is a smooth Kähler metric whose Ricci form equals the curvature form of the given metric. This is the prescribed-Ricci input recalled above. The proof proceeds by the continuity method for the complex Monge–Ampère equation.
** The same file's theorem <code>headline_dimensionZero</code> states the nonvanishing conclusion only in dimension zero. The nonvanishing theorem in positive dimension has no Lean statement in the collection.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 17 October 2026)
|-
| colspan="5" | No public follow-up work has been found.
|}

== Notes ==
* The library theorems above are not among the Comparator challenges of the collection, so the collection-wide kernel checks of the Comparator challenges do not cover them.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]