A section, eventually?

The claim, in plain words

On a complex manifold X, the anticanonical bundle −K_X is the top exterior power of the tangent bundle. When it is positive, as on a Fano manifold, its high powers have many sections: on the projective plane, 10, 28, 55 and 91 in degrees one to four. Suppose instead it only carries a smooth Hermitian metric of nonnegative curvature. That makes it nef, but it does not obviously give any section. In a positive-multiple form of a question Yau posed: must some power −mK_X, m > 0, have a nonzero section?

The multiple matters. On an Enriques surface E the canonical bundle is nontrivial but its square is trivial, so it has no section. On E times the projective line, the anticanonical bundle restricts to the canonical bundle of E and to degree two on each line; a Ricci-flat metric on E and the round metric on the line make it semipositive. It has no section, but its square has five, and it is not torsion.

For anticanonical bundles that are only nef, Lazić, Matsumura, Peternell, Tsakanikas and Xie proved numerical effectivity for threefold pairs, and Müller proved actual nonvanishing in dimension three, and in every dimension when the bundle is semiample on the fibers of the maximal rationally connected quotient. A smooth semipositive metric need not give semiampleness: blow up the plane at nine suitable points on a smooth cubic, and the anticanonical bundle has such a metric, yet no power of it is generated by its sections (Koike explains why).

Result 068 is seven OpenAI preprints, all dated September 26, 2026, 270 pages in all. The headline paper (27 pages) claims the answer in every dimension: if −K_X of a smooth connected complex projective variety has a smooth semipositive metric, then H⁰(X, −mK_X) ≠ 0 for some m > 0. The six companions give alternative routes and further results: a bounded-metric criterion for klt pairs, used on torus quotients; removing a fixed error from twisted sections while keeping invariance; invariant Euler characteristics; integrable metrics and effectivity; metric descent along fibrations; and exact orders of vanishing. Five reuse the headline paper’s structure theorem, and the last adds a second descent through a fibration of Matsumura and Wang.

What they don’t claim

The metric must be smooth and semipositive. Anticanonical bundles that are only nef, with no such metric, are not covered, and the headline theorem gives no bound on the power m.

Where it stands

Posted as preprints

OpenAI, seven papers, all dated September 26, 2026, released October 6

Peer reviewed

Not yet

Checked in Lean

Main theorem: no; OpenAI’s files hold large uncatalogued Lean developments for its inputs, including the case of Yau’s theorem the proof uses (we have not run them)

Last checked October 19, 2026. None of the seven preprints has been revised. The companions cite the headline paper, which cites none of them, and none cites papers from other results in the release. Inputs include Yau’s theorem, the structure theorems of Demailly, Peternell and Schneider and of Campana, Demailly and Peternell, the Bergman kernel positivity of Berndtsson and Păun, Berndtsson’s positivity of direct images, slope criteria for foliations, and hard Lefschetz with multiplier ideals. We found no public assessment by specialists. OpenAI published no Lean proof of the theorem in any positive dimension. Its files do contain uncatalogued (not linked from the collection’s catalog) Lean developments of 433 files and 53,544 lines, excluding Mathlib, with no unproved steps by our search; we have not run them. Most of it, 420 files and 48,549 lines, proves the case of Yau’s theorem that the headline paper uses: on a compact complex manifold with a projective embedding, the curvature of a smooth semipositive metric on the anticanonical bundle is the Ricci curvature of some Kähler metric. The rest are 10 files of side lemmas and three small files for the companions on exact orders and on controlled boundaries. The headline theorem is stated only in dimension zero, where it is trivial. Correction (October 15, 2026): the video says the Lean library has only a few uncatalogued files on side lemmas; there is far more, though still no proof of the theorem.

How the proof goes

1. Splitting the cover. Yau’s theorem turns the semipositive curvature into the Ricci form of a Kähler metric with nonnegative Ricci curvature. The universal cover then splits as flat space, times a compact Ricci-flat factor F, times a compact factor Z that is rationally connected and has no holomorphic forms.
2. The residual torus. The flat factor and F carry canonical frames, so the problem moves to Z. The deck transformations act on Z, possibly with infinite image; after a finite cover, the closure of that action is a compact torus. A torus-invariant anticanonical section on Z, multiplied by the frames, descends to a finite cover of X, and its norm, the product over the sheets, is a section on X.
3. Finite volume. On Z the paper proves, by induction on dimension, that if J = −K_Z + D has a semipositive metric of finite adjoint volume and L has a semipositive metric with bounded weights, then some aL + bD has a section. If not, a movable curve class α meets L and D trivially.
4. A smaller base. With no holomorphic forms, χ(O_Z) = 1; Riemann–Roch and hard Lefschetz give twisted forms whose determinants are sections of M + m_iL with m_i → ∞. A slope bound makes M·α ≤ 0, so no system of these sections is generically finite, and a maximal one defines a fibration onto a smaller base.
5. Moments. Fiber integrals move the problem to the base: the zeroth integral gives a finite-volume metric, and high moments, after taking roots, approach the fiberwise maximum and give a bounded metric. Induction produces a section that lifts with no forbidden poles.
6. Invariance. An invariant version of the transfer on a torus quotient, where a dense orbit makes the invariant relative sections one-dimensional and averaging is an orthogonal projection, gives the torus-invariant section.

The numbers in the video

• A short Python script checks the examples: on Enriques × P¹, h⁰(−mK) = 0, 5, 0, 9 for m = 1 to 4 while χ(−mK) = 2m + 1; χ(O) = 1 without holomorphic forms; the moments (∫ sin^2j πx dx)^1/j rising toward the maximum 1; on P¹, averaging over rotations keeps only the field z ∂/∂z; on P², only (xyz)^m is torus-invariant among the 10, 28, 55, 91 sections of −mK.

Read the source

• Anticanonical nonvanishing from smooth semipositivity (PDF), 27 pages.
• Invariant anticanonical indices and conversion of twisted differentials (PDF), 18 pages.
• Bounded anticanonical metrics on klt pairs and torus quotients (PDF), 20 pages.
• Cohomological transfer and equivariant anticanonical sections (PDF), 43 pages.
• Metric descent and rank-preserving contractions (PDF), 76 pages.
• Integrable metrics and effectivity with controlled boundary (PDF), 45 pages.
• Exact orders and invariant anticanonical linear systems (PDF), 41 pages. All dated September 26, 2026.
• The collection’s catalog, where this is result 068.

The 7 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

• Anticanonical nonvanishing from smooth semipositivity main paper
• Invariant anticanonical indices and conversion of twisted differentials companion
• Bounded anticanonical metrics on klt pairs and torus quotients companion
• Cohomological transfer and equivariant anticanonical sections companion
• Metric descent and rank-preserving contractions companion
• Integrable metrics and effectivity with controlled boundary companion
• Exact orders and invariant anticanonical linear systems companion

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.