Nef means symmetric?

The claim, in plain words

A vector bundle is nef if its tautological line bundle has nonnegative degree on every curve. Rational homogeneous varieties, the quotients G/P of a semisimple group by a parabolic subgroup, include projective spaces, quadrics, Grassmannians and flag varieties. The group’s vector fields span every tangent space, so their tangent bundles are generated by global sections and are nef. Mori showed that an ample tangent bundle forces projective space. In 1991 Campana and Peternell conjectured the analogue for nef: every Fano manifold with nef tangent bundle is rational homogeneous.

They proved it up to dimension three and for fourfolds of higher Picard number. Mok and Hwang finished the fourfolds using minimal rational curves, and Watanabe and Kanemitsu finished the fivefolds. Kanemitsu also proved it whenever the Picard number exceeds the dimension minus five. (A survey describes the state of the art in 2014.) For sixfolds that leaves Picard number one, and standard characterizations reduce to pseudoindex four or five, where the homogeneous examples are the Lagrangian Grassmannian LG(3,6) and the Grassmannian Gr(2,5).

Result 067 is one OpenAI preprint (27 pages, dated September 25, 2026). It claims the conjecture in dimension six: every smooth connected complex projective Fano sixfold with nef tangent bundle is rational homogeneous. Pseudoindex four had been treated by Watanabe; the paper gives an independent argument. The new step is pseudoindex five. With the structure theorem of Demailly, Peternell and Schneider, it also claims: a compact Kähler manifold with nef tangent bundle whose dimension minus its maximal irregularity is at most six has a finite cover whose Albanese map is a bundle with rational homogeneous fibers, and its universal cover is such a fiber times ℂ^q̃. In particular this holds in every dimension up to six.

What it doesn’t claim

Nothing about dimension seven or higher. The Kähler statement is not a separate proof: it follows from the sixfold theorem and the structure theorem of Demailly, Peternell and Schneider, and it needs the dimension minus the maximal irregularity to be at most six.

Where it stands

Posted as a preprint

OpenAI, dated September 25, 2026, released October 6

Peer reviewed

Not yet

Checked in Lean

No: OpenAI published no Lean proof of the theorem; uncatalogued Lean files check one supporting lemma about vector bundles (we have not run them)

Last checked October 19, 2026. The preprint has not been revised and cites no other paper from the release. It ships a Python certificate for its finite elimination; we ran it, and it printed pass. Inputs include Kanemitsu’s theorems, the theory of minimal rational curves of Hwang and Mok, Mok’s recognition theorem, Deligne’s fixed-part theorem and Grothendieck–Riemann–Roch. We found no public assessment by specialists. OpenAI published no Lean proof of the theorem. Its files do contain 17 uncatalogued (not linked from the collection’s catalog) Lean files, 4,630 lines excluding Mathlib, with no unproved steps by our search; we have not run them. They prove one supporting lemma about vector bundles on a family of projective lines: a bundle that is trivial on one fibre is trivial over a neighbourhood of it. The paper uses a statement of this kind, through cohomology and base change, in its Chern-class step. Correction (October 15, 2026): the video says there is no Lean formalization; that is still true of the theorem, but we missed these files.

How the proof goes

1. Minimal rational curves. For pseudoindex five, the rational curves of least anticanonical degree through a general point x form a smooth three-dimensional family F. Sending each curve to its tangent direction maps F to P(T_xX) ≅ P⁵; the image is the variety of minimal rational tangents. For Gr(2,5) it is the Segre threefold P¹ × P².
2. Two readings of one family. The universal family of the curves maps smoothly to X and to the space of curves. Read as a family of curves and as a family of threefolds over X, with Deligne’s fixed-part theorem and Grothendieck–Riemann–Roch, it yields linear and product identities among intersection numbers.
3. One quadratic. A finite rational elimination, with an exact certificate, leaves 32 − 20u + 3u² = 0, where u = c₁(T_F)·L²/L³ and L is the hyperplane class pulled back to F. So u is 4 or 8/3.
4. The Segre threefold. Hwang and Mok’s results force the image to span P⁵. The sectional genus 1 + L³(2 − u)/2 cannot be negative: u = 4 would give a linear three-space, which cannot span P⁵, and u = 8/3 gives L³ = 3 and genus 0. A threefold of degree three spanning P⁵ is a scroll of minimal degree, and smoothness of F leaves only the Segre threefold. Mok’s recognition theorem then identifies X with Gr(2,5).
5. Pseudoindex four. Kanemitsu’s factorization, Hard Lefschetz and intersection theory rule out the possible fibers; the last case, an odd-dimensional quadric bundle, would give an integral divisor a non-integral degree.

The numbers in the video

• A short Python script lists, from root data, the rational homogeneous sixfolds of Picard number one (P⁶, Q⁶, Gr(2,5) and LG(3,6), of index 7, 6, 5 and 4), solves 3u² − 20u + 32 = 0, runs the two sectional-genus cases, and computes L³ = 3, c₁·L² = 8 and genus 0 for the Segre threefold.

Read the source

• The Campana–Peternell conjecture in dimension six (PDF), September 25, 2026 (27 pages).
• The certificate script for the finite elimination.
• Watanabe, Fano manifolds of coindex three admitting nef tangent bundle (arXiv).
• A survey on the Campana–Peternell conjecture (arXiv).
• The collection’s catalog, where this is result 067.

The paper

OpenAI groups related papers into one result; this one has a single paper.

• The Campana–Peternell conjecture in dimension six

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.