AI Proved What?

Episode 036, October 2026

Semiample, numerically?

Numerical semiampleness and generalized minimal models

Covers result 036 in OpenAI’s catalog: all 4 papers. See its connections to other results and the work it cites.

Play Episode 036: Semiample, numerically? Generalized abundance with a nef divisor added. The curve y squared equals x cubed plus 17 with orange multiples of a point of infinite order, under K plus B plus M numerically equivalent to semiample.

5:09. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Adding a nef divisor
  2. 1:11What was known
  3. 2:05The claim
  4. 3:19How the proof goes
  5. 4:25Where it stands

The claim, in plain words

The abundance conjecture (our episode 034) asks whether a nef adjoint K + B is semiample. Add a nef divisor M, as in a generalized pair, and semiampleness can fail already on an elliptic curve: for a point P of infinite order, M = 𝒪(P − O) is nef but no positive multiple has a section. It is, however, numerically trivial. Lazić and Peternell conjectured in 2018 that K + B + M is always numerically equivalent to a semiample divisor.

Result 036 has four preprints. The central one (37 pages) claims this generalized abundance conjecture for projective klt pairs over any algebraically closed field of characteristic zero, with K + B pseudo-effective, M a nef ℚ-Cartier divisor on X and K + B + M nef; on a klt Calabi–Yau pair every nef divisor is then numerically semiample, which is Lazić and Peternell’s semiampleness conjecture. Companions claim a Kähler version with Bott–Chern classes, minimal models or Mori fibre spaces for generalized log canonical pairs (the existence form of the minimal model conjecture, ordinary log canonical pairs included), and minimal models in numerical dimension one.

What it doesn’t claim

The conclusion is numerical: K + B + M has the same degrees on every curve as a semiample divisor, not that it is semiample itself. The nef summand must be a divisor on X, not an arbitrary nef b-divisor on a higher model. The minimal-model paper gives a terminating choice of program, not termination of every program.

Where it stands

Posted as preprints
OpenAI, four papers dated September 24 to October 6, 2026, released October 6
Peer reviewed
Not yet
Checked in Lean
No: OpenAI published no Lean proof of the main theorems; an uncatalogued supporting library for the numerical-dimension-one paper exists (we have not run it)

Last checked October 19, 2026. None of the papers has been withdrawn; the Kähler paper was revised in the October 7 update to state its inputs explicitly. The central paper depends on log abundance (result 034) and on the generalized minimal-model paper; the Kähler paper also uses the central paper and Iitaka subadditivity (result 033). We found no public assessment by specialists. OpenAI published no Lean proof of the main theorems. Its files do contain an uncatalogued (not linked from the collection’s catalog) supporting library for the numerical-dimension-one paper: 51 files and 29,042 lines, excluding Mathlib, with no unproved steps by our search; we have not run it. It proves ingredients such as a negativity lemma for exceptional divisors, a multiplier-ideal pushforward on a simple-normal-crossing model, and the absence of quadratic section growth when κσ = 1. It does not prove that the minimal model exists: the library defines that statement but never proves it. Correction (October 15, 2026): the video says there is no Lean proof; that is still true of every main theorem, but we missed this library.

What was known

  • With M = 0 the statement is ordinary klt abundance, by Fukuda’s theorem that a numerically semiample K + B is semiample.
  • Lazić–Peternell: surfaces, and threefolds with K + B of positive numerical dimension; in higher dimensions a reduction to abundance, termination of flips and, for numerical dimension zero, a semiampleness conjecture for Calabi–Yau pairs.
  • Chaudhuri: cases of low nef dimension of the sum. Fontanari: actual semiampleness on surfaces in a case.

How the proof goes

  1. Inputs and reduction. Using log abundance and the generalized minimal model programs, two compatible programs run in turn: one makes K + B semiample, the next makes a nearby K + B + M nef. Positive Kodaira dimension allows induction on the fibres.
  2. Full nef dimension implies big. On a Calabi–Yau pair, a nef divisor with positive degree on every curve through a very general point is big: otherwise rescaled ample approximations of bounded volume would have unbounded degrees on very general curves, against curves of bounded degree from Birkar–Zhang.
  3. The clash. As in the abundance paper, a small bound on vanishing orders on the variety conflicts with a large system of jets on a projective bundle over its square; a Frobenius comparison after reduction to characteristic p rules this out.

The numbers in the video

  • On y² = x³ + 17, the point P = (−2, 3) has 2P = (8, −23); since 23² does not divide 27·17², the Nagell–Lutz test shows P has infinite order. A short Python script computes mP exactly for m up to 12; the denominators reach 28 digits.

Read the source

The 4 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.

Transcript

Read the full script

0:00Adding a nef divisor

Our abundance episode asked: if K + B is nef, is it semiample? There’s a natural generalization. A generalized pair carries one more nef divisor, M. It comes, for example, from the canonical bundle formula of a fibration, whose moduli part records how the fibers vary. In the conjecture, M is a nef divisor on X itself. So ask: if K + B is pseudo-effective, M is nef, and the sum K + B + M is nef, is the sum semiample? Not always, already on a curve. On the elliptic curve y² = x³ + 17, let M be the degree-zero line bundle of the point (−2, 3). The point’s multiples never return to the origin, so no positive multiple of M has a section. M is nef, but not semiample. Yet M has degree zero on every curve, just like the trivial bundle, which is semiample. Numerically, you can’t tell them apart. So Vladimir Lazić and Thomas Peternell, in 2018, conjectured exactly that much: K + B + M should be numerically equivalent to a semiample divisor. This is the generalized abundance conjecture.

1:11What was known

When M is zero, it’s the ordinary abundance conjecture, because Fukuda showed that a numerically semiample K + B is semiample. Lazić and Peternell proved the conjecture for surfaces, and for threefolds when K + B has positive numerical dimension. In higher dimensions they reduced it to abundance, termination of flips, and, when K + B has numerical dimension zero, a semiampleness conjecture for Calabi–Yau pairs. Chaudhuri settled cases where the sum has low nef dimension, and Fontanari sharpened the surface case. That Calabi–Yau case is the heart of it. When K + B is numerically trivial, everything rests on the nef divisor M. Suppose M has positive degree on every curve through a very general point: full nef dimension. Must M then be big, with positive volume?

2:05The claim

Result 036 has four OpenAI preprints. The central one, 37 pages, dated October 3, claims a proof of the generalized abundance conjecture for projective klt pairs over any algebraically closed field of characteristic zero. If K + B is pseudo-effective, M is nef, and K + B + M is nef, then it is numerically equivalent to a semiample divisor. On a klt Calabi–Yau pair, every nef divisor is then numerically semiample: exactly the semiampleness conjecture of Lazić and Peternell. A 52-page companion claims a Kähler version, for smooth compact Kähler manifolds with a simple normal-crossing boundary, using Bott–Chern cohomology. A 79-page paper claims the existence of minimal models for projective generalized log canonical pairs, or Mori fiber spaces when the adjoint is not pseudo-effective, including ordinary log canonical pairs: the existence form of the minimal model conjecture. And a 14-page paper claims minimal models for smooth varieties in numerical dimension one.

3:19How the proof goes

The central paper leans on two companions from the release: log abundance, our result 034, and the minimal model programs of the generalized-pair paper. Following Lazić and Peternell, it runs two compatible programs in turn, keeping a semiample ordinary adjoint and a nearby nef generalized one. When the Kodaira dimension is positive, induction on the fibers takes over. What remains is a Calabi–Yau pair, and the key new step: a nef divisor of full nef dimension there is big. If it weren’t, ample approximations could be rescaled to bounded volume, while their degrees on very general curves grow without bound. A theorem of Birkar and Zhang supplies curves of bounded degree, and that conflict controls moving jets. As in the abundance paper, the argument ends in a clash: a small bound on vanishing orders on the variety itself, against a large system of jets on a projective bundle over its square. After reduction to characteristic p, a Frobenius comparison shows the two can’t both hold.

4:25Where it stands

These are preprints, not yet peer reviewed, with no Lean proof. The central paper depends on companion results in the same release, log abundance and the generalized minimal model paper, so it stands or falls with them. The Kähler paper also uses the central paper and Iitaka subadditivity, and it was revised in OpenAI’s October 7 update, to state its inputs explicitly. We found no public assessment by specialists. If the proofs hold, abundance extends, up to numerical equivalence, to klt pairs with a nef divisor added: the nef adjoint has the same degrees as one that comes from a map.

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.