AI Proved What?

Episode 034, October 2026

Always semiample?

The log abundance conjecture, projective and compact Kähler

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

Play Episode 034: Always semiample? The abundance conjecture in every dimension. The real points of the elliptic curve y squared equals x cubed plus 17 with orange dots at multiples of the point (minus 2, 3) scattered along it, under the question whether K plus B nef implies semiample.

6:22. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Minimal models
  2. 0:59Nef versus semiample
  3. 2:32The claim
  4. 3:37How the proof goes
  5. 5:20Where it stands

The claim, in plain words

A line bundle is nef if its degree on every curve is nonnegative, and semiample if some multiple is generated by its sections, which then define a map. Every semiample bundle is nef, but not conversely: on an elliptic curve, the degree-zero bundle of a point P minus the origin is semiample only when P is a torsion point. The abundance conjecture says that this never happens for the canonical class: on a log canonical pair (X, B), if KX + B is nef, it is semiample.

Result 034 is a family of fourteen preprints. The core one, Log abundance in characteristic zero (September 24, 85 pages), claims log abundance with effective rational boundary in every dimension over every algebraically closed field of characteristic zero, and, over the complex numbers, nonvanishing: a pseudo-effective canonical class has a nonzero pluricanonical form. Its induction gives good minimal models for every complex projective log canonical pair with pseudo-effective adjoint. A 157-page companion extends abundance to compact Kähler spaces, assuming logarithmic Iitaka subadditivity (episode 033). Others claim the effective Iitaka fibration conjecture and uniform indices for semi-log-canonical log Calabi–Yau pairs.

What it doesn’t claim

Positive characteristic is not covered by these papers (other results in the release treat threefolds in characteristic p), and the boundary coefficients must be rational for the abundance statement. The compact Kähler theorem is conditional on logarithmic Iitaka subadditivity.

Where it stands

Posted as preprints
OpenAI, 14 papers; the core one dated September 24, 2026 (85 pages); released October 6
Peer reviewed
Not yet
Checked in Lean
No: OpenAI published no Lean proof of the main theorems; uncatalogued Lean files check supporting steps of two companion papers (we have not run them)

Last checked October 19, 2026. In OpenAI’s October 7 update the Kähler paper (first version October 4) and a conditional fourfold paper were revised; the projective paper was not. That fourfold paper’s appendix presents the same projective argument as “a positive conditional resolution of the log abundance conjecture”, conditional on logarithmic Iitaka subadditivity, although it too uses that assumption only in an Albanese step which the projective paper says also follows from a theorem of Hacon, Popa and Schnell. VibeMathed lists the claim as contested for that reason. We found no assessment by specialists. OpenAI published no Lean proof of the main theorems. Its files do contain 18 uncatalogued (not linked from the collection’s catalog) Lean files, 5,763 lines excluding Mathlib, with no unproved steps by our search; we have not run them. Sixteen (5,114 lines) prove an algebraic step of the companion on relative denominators: section ratios of an adjoint divisor recover the function field of the base. Two (649 lines) prove local integrability and gauge lemmas for the companion on minimal metrics; they say themselves that they prove neither its metric theorem nor its injectivity theorem. Correction (October 15, 2026): the video says there is no Lean proof; that is still true of every main theorem, but we missed these files.

What was known

  • Curves and surfaces (classical). Threefolds: Miyaoka (numerical dimension one, 1988) and Kawamata (1992); log threefolds: Keel, Matsuki and McKernan (1994); semi-log-canonical threefolds: Fujino.
  • Minimal models of general type: the base-point-free theorem of Kawamata and Shokurov. Numerically trivial adjoints: Nakayama, Gongyo. Numerical dimension at most one in dimension at most five: Liu and Xu.
  • The minimal model program: Mori (threefolds, 1988); Birkar, Cascini, Hacon and McKernan (general type, 2010). From dimension four on, abundance and even nonvanishing were open.

How the proof goes

  1. Induction on dimension. Assuming good models in lower dimension, first prove nonvanishing for smooth varieties, then make log minimal models good.
  2. A signed-boundary criterion. If a nef dlt adjoint L = KX + D is a combination of boundary components with coefficients of either sign and is semiample on the whole boundary, then κ(L) = ν(L). A root construction separates the positive part, a Hodge-module calculation lifts local parameters through every infinitesimal neighbourhood (as in Miyaoka’s threefold argument), boundary fibres deform into the interior to give a covering family on which L is trivial, and the nef reduction finishes.
  3. Nonvanishing by contradiction. In a counterexample, a nonconstant Albanese map is ruled out by Iitaka subadditivity (its one use; also covered by Hacon–Popa–Schnell), and positive currents and bounds on curves rule out two special kinds of covering family.
  4. A clash of estimates. On one copy of the variety, sections vanish only to a limited order at a very general point; on the product of two copies they separate many jets. After reduction modulo a large prime, comparing ordinary and Frobenius jets on the diagonal forces a determinant to vanish to higher order than allowed.

The numbers in the video

  • On y² = x³ + 1, the point (2, 3) has order 6: (2, 3), (0, 1), (−1, 0), (0, −1), (2, −3), then the origin.
  • On y² = x³ + 17, the point P = (−2, 3) has 2P = (8, −23), and 23² does not divide 27·17², so by the Nagell–Lutz theorem P is not a torsion point. A short Python script computes mP exactly for m ≤ 12; the denominators reach 28 digits.

Read the source

The 14 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:00Minimal models

Algebraic geometers classify varieties up to birational change: two count as the same if they agree once you remove some lower-dimensional pieces. So the first job is to choose a best representative in each class. Blowing up a point on a surface replaces it with a curve E whose self-intersection is minus one. The canonical class K meets E negatively, in minus one, so K is not nef. Nef means nonnegative on every curve. Castelnuovo’s theorem lets you contract such curves, undoing the blowups. What remains is a minimal surface with K nef, unless the surface is ruled. The minimal model program does this in higher dimensions: Mori for threefolds, in 1988, and Birkar, Cascini, Hacon and McKernan in 2010 for varieties of general type. The program aims to end with either a nef canonical class, or a fibration by simpler pieces of Fano type.

0:59Nef versus semiample

Nef is a numerical condition. Semiample is geometric: some multiple of the line bundle is generated by its sections, so those sections define a map. Every semiample bundle is nef, but not the other way around. On an elliptic curve, take the line bundle of a point P minus the origin. Its degree is zero, so it’s nef. A multiple of it has a section only if that multiple of P is the origin. On y² = x³ + 1, the point (2, 3) returns to the origin after six steps, so six times the bundle is trivial: semiample. On y² = x³ + 17, the point (−2, 3) never returns. The Nagell–Lutz test rules it out at 2P, and the denominators of its multiples keep growing. That bundle is nef, but never semiample. The abundance conjecture says this never happens for the canonical class. On a log canonical pair, if K + B is nef, then it’s semiample. Its sections then give the Iitaka fibration as an honest map, and the Kodaira dimension equals the numerical dimension. It’s known for curves and surfaces. For threefolds it’s due to Miyaoka and Kawamata, and for log threefolds to Keel, Matsuki and McKernan. For minimal models of general type, it’s the base-point-free theorem of Kawamata and Shokurov. From dimension four on it has been open, along with the weaker nonvanishing conjecture: that some multiple has a section at all.

2:32The claim

Result 034 is a family of fourteen OpenAI preprints. At its core is an 85-page paper, dated September 24. It claims that in characteristic zero, in every dimension, a nef log canonical divisor with rational boundary, on a projective log canonical pair, is semiample. Over the complex numbers it also claims nonvanishing for smooth projective varieties: a pseudo-effective canonical class has a nonzero pluricanonical form. Over the complex numbers, its induction gives good minimal models for every projective log canonical pair with a pseudo-effective adjoint, and, with a companion paper, finite generation of rational log canonical rings. A 157-page companion extends abundance to compact Kähler spaces, assuming the logarithmic Iitaka subadditivity from our previous episode. Others claim the effective Iitaka fibration conjecture, and uniform indices for log Calabi–Yau pairs.

3:37How the proof goes

The proof is an induction on dimension, with two tasks in each dimension. First prove nonvanishing. Then use it to make minimal models good, meaning that the adjoint becomes semiample. Both tasks use a criterion about the boundary. Suppose the nef adjoint is a combination of boundary components, with coefficients of either sign, and is already semiample on the whole boundary. Then its Kodaira dimension equals its numerical dimension. To prove it, a root cover separates the positive and negative parts, and a Hodge-module calculation lifts local parameters through every infinitesimal neighborhood of the boundary, an idea that goes back to Miyaoka. Pieces of the boundary then deform into the interior, sweeping out the variety with subvarieties on which the adjoint is trivial, and the nef reduction finishes the argument. Nonvanishing is proved by contradiction. In a counterexample, a nonconstant Albanese map is ruled out first. This is the paper’s one use of Iitaka subadditivity, and it notes that this case also follows from a theorem of Hacon, Popa and Schnell. Positive currents and bounds on curves then rule out two special kinds of covering family. What’s left is a clash of two estimates at a moving point. On one copy of the variety, sections can vanish there only to a limited order. On the product of two copies, they separate many jets. Reducing modulo a large prime, the paper compares ordinary jets with Frobenius jets along the diagonal, and a determinant then has to vanish to a higher order than the first estimate allows. The contradiction gives nonvanishing.

5:20Where it stands

These are preprints, not yet peer reviewed, and there’s no Lean proof. In OpenAI’s October 7 update, the Kähler abundance paper and a related fourfold paper were revised, adding arguments and spelling out hypotheses. The 85-page projective paper hasn’t been revised. There’s a tension inside the release. The projective paper states abundance unconditionally, but an appendix to the fourfold paper presents the same argument as conditional on logarithmic Iitaka subadditivity, even though it, too, uses it only in the Albanese step, which the projective paper says Hacon, Popa and Schnell already cover. One public tracker lists the claim as contested for that reason. We found no assessment by specialists. If the proof holds, it settles a central conjecture of the minimal model program: every complex projective log canonical pair with a pseudo-effective adjoint has a good minimal model.

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.