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 (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_X makes the anticanonical class nef. The nonvanishing question asks whether H⁰ of −mK_X is nonzero for some integer m > 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_X 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 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_X admits a smooth Hermitian metric of semipositive curvature, then H⁰ of −mK_X is nonzero for some integer m > 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 1581d4c of the openai/math repository, folder 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 (lean/docs/) or Comparator challenge for this family.
  • The repository's Lean library contains a theorem prescribedRicciFromSemipositive in 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 headline_dimensionZero 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

Date	Work	Relation	Public claim	Public status (checked 17 October 2026)
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.