AI Proved What?

Episode 052, October 2026

Split tangent, split space?

Tangent splittings and product decompositions

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

Play Episode 052: Split tangent, split space? A rectangle crossed by blue horizontal and orange vertical lines, with a white tangent vector split into a blue and an orange arrow, above TX = E1 plus E2 implies the universal cover is Y1 times Y2.

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

Chapters

  1. 0:00Products and splittings
  2. 1:23The claim
  3. 2:18Continuing local products
  4. 4:06Rational curves force integrability
  5. 5:16Where it stands

The claims, in plain words

On a product Y1 × Y2, every tangent vector splits into a part along each factor, so the tangent bundle is a direct sum E1 ⊕ E2, and each piece is integrable: its directions fit together into leaves. The converse asks whether a holomorphic splitting TX = E1 ⊕ E2 of a complex manifold comes from a product, matching the given pieces. Integrability is needed: Beauville’s example on an abelian surface times a projective line has a complement to the line direction that is not integrable. In a paper published in 2000, Beauville conjectured that on a compact Kähler manifold whose tangent bundle splits into two integrable pieces (with more pieces, every partial sum integrable), the universal cover is a product whose factors carry those pieces. He proved it for Kähler–Einstein manifolds and for surfaces; later work handled a line summand, a flat summand, or a compact leaf with finite holonomy. On rationally connected manifolds, Höring showed that one integrable summand already gives a product, and conjectured that there the summands are always integrable (stated as Conjecture 1.5 in his 2026 preprint).

Result 052 is two OpenAI preprints dated September 23, 2026. The first (33 pages) claims Beauville’s conjecture for two summands: if a compact connected Kähler manifold of dimension at least two has TX = E1 ⊕ E2 with both summands integrable and of positive rank, its universal cover is biholomorphic to a product Y1 × Y2 of simply connected manifolds, with the lifted Ei as the factor directions. The factors are the universal covers of the leaves through a point and can be noncompact. The second (16 pages) claims that on a smooth rationally connected projective manifold, both summands of every holomorphic splitting into two positive-rank pieces are integrable; with Höring’s theorem, the manifold is then an actual product X1 × X2 matching the split.

What they don’t claim

The first paper is about the ordinary universal cover: it does not say that a finite cover of X is a product, and it treats two summands, not the general multi-summand conjecture. The second needs smoothness: Höring gives a singular rationally connected variety with a non-integrable summand.

Where it stands

Posted as preprints
OpenAI, both dated September 23, 2026, released October 6
Peer reviewed
Not yet
Checked in Lean
Both main theorems, by OpenAI (scope note); we have not run the check

Last checked October 19, 2026. Neither preprint has been withdrawn or revised, and they cite no other paper from the release except each other. OpenAI’s Lean formalizations cover the two main theorems: the universal-cover product for two integrable summands (about 15,000 lines in 46 files) and integrability on rationally connected manifolds (about 17,300 lines in 15 files), not counting Mathlib. Since Mathlib lacks this geometry, the formal statements (the first, the second) define Kähler metrics, holomorphic splittings, integrability and rational connectedness themselves. The corollaries, including the product decomposition for rationally connected manifolds, are outside the Lean scope. We found no public assessment by specialists.

How the proofs go

  1. Product charts. Integrability gives local coordinates (z1, z2) with Ei along zi; on overlaps the new z1 depends only on the old z1, and likewise for z2. The task is to continue these local products globally.
  2. Holomorphic boxes. A box is a map f(s, t) whose s-derivative lies in E1 and t-derivative in E2; in a chart it is (f1(s), f2(t)). A box on a Hartogs figure extends to the filled region: an extension theorem for maps into compact Kähler manifolds gives a meromorphic extension, and the two tangencies forbid a point spreading into a curve. A box can also be pushed across a convex boundary where the complex tangent mixes both variables: Stokes’ theorem for the closed Kähler form bounds areas of small discs, one of many small annuli has tiny area, and a Hartogs shell built from it reaches past the boundary.
  3. Grids and monodromy. Two discs through a point, one in each leaf, span a box on the whole bidisc. Grids of boxes turn a path in each leaf into the edges of a rectangle, and any path into the diagonal of one, so the local product map and its inverse continue along every path; on simply connected covers this gives the product.
  4. Tangent boxes on ℙ¹ × ℙ¹. For the second paper, any rational curve g gives F: ℙ¹ × ℙ¹ → X with F(s, s) = g(s) and the two tangencies, with no integrability assumed: a formal solution along the diagonal, a section count showing it comes from a rational map, and a resolution in which the tangencies contract every exceptional curve.
  5. The obstruction dies. Along a factor line the complementary summand is trivial, so the bracket obstruction Pj[e, e′] on two sections is constant there. Rational connectedness supplies sections vanishing at one marked point and spanning at another, so the obstruction vanishes on an open set and hence everywhere.

The numbers in the video

  • A short symbolic script checks Beauville’s example (the bracket [U + S, V + T] = ∂w is vertical and leaves the span), the product form of boxes, a tangent box for a Möbius map on ℙ¹ × ℙ¹, and the formal recursion along the diagonal to order six. The Lean line counts are our counts of the import closures of the two proof modules.

Read the source

The 2 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:00Products and splittings

On a product of two manifolds, every tangent vector splits into a part along the first factor and a part along the second. The tangent bundle is a direct sum, and each piece is integrable: its directions fit together into leaves, the copies of each factor. The converse asks: if the tangent bundle of a complex manifold splits into two holomorphic pieces, does the manifold come from a product? Integrability is needed. Beauville’s example on an abelian surface times a projective line tilts the surface directions by two vector fields on the line that don’t commute, and the tilted directions are not integrable. In a paper published in 2000, Beauville conjectured that integrability is enough, after passing to the universal cover. For two pieces: on a compact Kähler manifold whose tangent bundle splits into two integrable pieces, the universal cover is a product whose factors carry those pieces. With more pieces, every combination of pieces has to be integrable too. He proved it for Kähler-Einstein manifolds and for surfaces. Later work handled a line summand, a flat summand, or a compact leaf with finite holonomy. For rationally connected manifolds, Höring showed that one integrable summand already gives a product, and he conjectured that there the summands are always integrable.

1:23The claim

Result 052 is two OpenAI preprints, both dated September 23. The first, 33 pages, claims Beauville’s conjecture for two summands. If a compact connected Kähler manifold has its tangent bundle split into two integrable holomorphic subbundles of positive rank, then its universal cover is a product of two simply connected manifolds, matching the split. The factors are the universal covers of the leaves through a point, and they can be noncompact. The second, 16 pages, claims that on a smooth rationally connected projective manifold, both summands of any holomorphic splitting are automatically integrable. Combined with Höring’s theorem, such a manifold is then literally a product, matching the split. Smoothness matters: Höring has a singular rationally connected example where integrability fails.

2:18Continuing local products

Start with the first paper. Integrability gives local product charts: near each point, two groups of coordinates, z₁ and z₂, with the first piece along z₁ and the second along z₂. Where two such charts overlap, the new z₁ depends only on the old z₁, and the new z₂ only on the old z₂. The problem is to continue these local products globally: to transport a path in one leaf all the way along a path in the other. The paper’s tool is a holomorphic box: a map of two variables, s and t, whose s-direction stays in the first piece and whose t-direction stays in the second. In a product chart it is just f₁(s) next to f₂(t). First, a box on a Hartogs figure extends to the filled region. An extension theorem for maps into compact Kähler manifolds gives a meromorphic extension, which might spread a single point out into a whole curve, but the two tangencies rule that out. Second, a box can be pushed across the boundary of a convex domain, wherever the boundary’s complex tangent direction mixes both variables. Stokes’ theorem for the closed Kähler form bounds the areas of small discs, and among many small annuli one has tiny area, so its image fits in a single product chart. From it the paper builds a Hartogs shell that reaches past the boundary, and fills it. Together, two discs through the same point, one in each leaf, span a box on the whole bidisc. Grids of these boxes turn a path in one leaf and a path in the other into the edges of a rectangle, and any path in the manifold into the diagonal of one. So the local product map and its inverse continue along every path. On simply connected covers the continuation doesn’t depend on the path, and it gives the product.

4:06Rational curves force integrability

The second paper needs no integrability to start. Given any rational curve g in the manifold, it builds a tangent box: a map F from the product of two projective lines, equal to g on the diagonal, with the first direction in the first piece and the second direction in the second. It solves for F as a power series along the diagonal, shows by counting sections that the series comes from a rational map, and then the tangencies force every exceptional curve of a resolution to collapse, so F is holomorphic everywhere. Along a factor line of the box, the complementary piece becomes a trivial bundle. Now take the bracket of two sections of one piece and project it to the other piece: that is the obstruction to integrability. On a factor line it is a section of a trivial bundle on the projective line, so it is constant. Rational connectedness supplies sections that vanish at one marked point and span the piece at another. The constant vanishes at the first point, so it vanishes at the second. Those second points fill an open set, so the obstruction vanishes there, and hence everywhere.

5:16Where it stands

Both are preprints, not yet peer reviewed, and neither has been revised. OpenAI published Lean formalizations of the two main theorems, about 15,000 and 17,000 lines, not counting Mathlib. Since Mathlib lacks this geometry, the formal statements define Kähler metrics, holomorphic splittings and rational connectedness themselves. We haven’t run the check. The corollaries, including the product decomposition for rationally connected manifolds, are outside the Lean scope. We found no public assessment. If they hold, on compact Kähler manifolds any splitting of the tangent bundle into two integrable pieces comes from a product on the universal cover, and on smooth rationally connected manifolds any splitting into two holomorphic pieces comes from an actual product.

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.