Split tangent bundles and product decompositions

Split tangent bundles and product decompositions concerns a converse to the splitting of the tangent bundle of a product: if the holomorphic tangent bundle of a compact complex manifold X is a direct sum T_X = E₁ ⊕ E₂ of subbundles, is the universal cover a product whose factor directions are the two given summands? Two manuscripts in OpenAI's public mathematics collection, both dated 23 September 2026, claim the two-summand case of Beauville's conjecture for compact Kähler manifolds with integrable summands, and the integrability of both summands of every splitting on a smooth rationally connected projective manifold, which with a theorem of Höring makes such a manifold a compatible product. The collection's Lean formalization covers both main theorems.

Background

• As recounted in the manuscripts' introductions:
  • The question. The product must be compatible with the specified subbundles, not only abstractly a product, and each summand must be integrable. An example on the product of an abelian surface with the projective line, discussed by Beauville and by Höring, has a complement to the line direction that is not integrable. Holomorphic Frobenius gives local product coordinates for integrable summands; the problem is to continue them globally.
  • Beauville's conjecture. Beauville formulated the compatible universal-cover conjecture for compact Kähler manifolds whose summands have integrable partial sums, and proved it for Kähler–Einstein manifolds, refining an earlier result of Yau, and for compact Kähler surfaces. Later cases are due to Druel for projective manifolds whose tangent bundle is a sum of line bundles, to Brunella, Pereira and Touzet for a line summand with integrable complement, to Pereira and Touzet for a Hermitian flat summand, and to Druel, Pereira, Pym and Touzet for numerically flat foliations and for a foliation with a compact leaf of finite holonomy.
  • Integrability. Höring proved automatic integrability on non-uniruled projective manifolds, using a positivity theorem of Campana and Peternell and an integrability theorem of Demailly. On the rationally connected side, Campana and Peternell treated Fano manifolds with a summand of rank one or two; Höring showed that one integrable summand already gives a compatible product and conjectured that a summand is always integrable. His 2026 work proves algebraic integrability on klt varieties of Fano type and gives a singular rationally connected example with a nonintegrable summand.

The original results

• Universal-cover splitting, 23 September 2026. The main theorem of Universal-cover splitting for compact Kähler manifolds states that for a compact connected Kähler manifold X of dimension n ≥ 2 with a specified decomposition T_X = E₁ ⊕ E₂ into integrable holomorphic subbundles of positive ranks, the ordinary universal cover is biholomorphic to a product Y₁ × Y₂ of connected simply connected complex manifolds, the differential carrying the pullback of each E_i to the tangent bundle of the factor Y_i. The manuscript describes this as the two-summand form of Beauville's compatible splitting conjecture. Through Höring's integrability theorem it derives the compatible product for every splitting on a non-uniruled projective manifold, and for projective manifolds with nef and big canonical bundle it also shows that the canonical Kähler–Einstein connection preserves both summands on the regular canonical locus.
• Automatic integrability, 23 September 2026. The main theorem of Integrability of split tangent bundles on rationally connected manifolds states that on a smooth connected rationally connected projective complex manifold of dimension at least two, both summands of every specified holomorphic splitting into positive-rank subbundles are integrable. The manuscript states that this proves the smooth rationally connected assertion of Höring's Conjecture 1.5 of 2026, and that with Höring's earlier product theorem it gives an isomorphism X ≅ X₁ × X₂ with smooth projective factors that identifies the summands with the factor tangent bundles. It also applies the theorem to general fibers of the rationally connected quotient of a uniruled compact Kähler manifold.
• Scope, as stated: the Kähler theorem concerns the ordinary universal cover, whose factors can be noncompact; it does not assert that a finite cover of X is a product. Both theorems treat splittings into two summands. The rationally connected theorem needs smoothness, as Höring's singular example shows.
• Method, as described: for the Kähler theorem, holomorphic boxes are maps of two scalar parameters whose derivatives lie in E₁ and E₂. A Hartogs figure is filled by a box through Ivashkovich's meromorphic extension theorem, and a convex boundary is crossed using area bounds from Stokes' theorem for the Kähler form. Polydisk boxes and rectangular grids then continue the local product map and its inverse along arbitrary paths, and monodromy gives the biholomorphism of the universal covers; the appendices give a second continuation method through the canonical contraction. For the rationally connected theorem, each rational curve is extended along the diagonal to a tangent box on the product of two projective lines, built from a formal solution whose coordinate ratios are shown to be rational. A projected-bracket partial connection transports the summands along the box, and a two-point family of rational curves forces the bracket tensor of each summand to vanish.
• Sources. Commit adc7f12 of the openai/math repository: Universal-cover splitting for compact Kähler manifolds and Integrability of split tangent bundles on rationally connected manifolds.
• Formalization. The scope note states that the Lean development proves the universal-cover product for a compact connected Kähler manifold whose tangent bundle splits into two positive-rank integrable holomorphic subbundles, with factors of the prescribed dimensions and the differential identifying the tangent factors with the summands; automatic integrability and the paper's corollaries are not included there. It also proves integrability of both summands for a compact connected complex manifold of dimension at least two with a projective embedding witnessing rational connectedness; the compatible product decomposition is outside this selected statement. Comparator statements: KahlerSplitting.lean and SplitTangentIntegrability.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 31 October 2026; AI Proof Watch rows 1 November 2026)
2026-10-08	MathVet, a GitHub review of openai/math, tables at repository commit c76f1e4 of 14 October 2026	Review, fidelity of the formal statement	Rates this family "full": both headline theorems are stated, while the product decomposition for rationally connected manifolds, which composes the two results and needs a Kähler metric from the embedding, is not a single statement. Among the definitions to check it lists bespoke encodings of complex manifolds, Kähler metrics, integrability, the ordinary universal cover, compatible products, projective embeddings and rational connectedness, plausible but unchecked against standard notions. It records sandboxed Comparator passes for both challenges on 8 October 2026, with dependency cones of about 15,000 and 17,300 lines.	Review repository. Read on 31 October 2026.
2026-10-10	cert-machine, openai/math lane K, run 38051470892	Verification, two kernels	Records the challenges KahlerSplitting and SplitTangentIntegrability as certified: Lean's default kernel and the nanoda kernel both accept the solutions, in 562 s and 543 s. C. Toledo's report lists the lane's results.	Repository. The run concerns the formalized statements only.
2026-10-10 to 2026-10-14	con-leche development journal, task #348	Verification, second kernel	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list this family's two challenges, so they were accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-12	AI Proved What?, episode 052 Split tangent, split space?, remade version of 26 October 2026	Reading, exposition	Video explainer of the two preprints, of 33 and 16 pages. It recalls Beauville's conjecture, the cases proved by Beauville and the later cases of a line summand, a flat summand and a compact leaf with finite holonomy, and Höring's work on rationally connected manifolds. It states that the first paper concerns the ordinary universal cover, does not say that a finite cover is a product and treats two summands, not the general multi-summand conjecture, and that the second needs smoothness.	Episode status, last checked 30 October 2026: posted as preprints, released 6 October, not withdrawn or revised; under expert review, not yet; peer reviewed, not yet; checked in Lean, both main theorems, by OpenAI, which the site did not run; no public assessment by specialists found. It notes that the Lean files define Kähler metrics, splittings, integrability and rational connectedness themselves, and that the corollaries are outside the Lean scope. The site states that it is made with Anthropic's Claude. Read on 31 October 2026.
2026-10-16	J. Jardine, Lattice24, referee review rank_442 of the rationally connected manuscript, in JJardine919/openai-math-audit	Review, AI-assisted audit	Reports no gap and lists no issues. It states that the reviewer read every section, including both appendices, and checked by hand, among other steps, the formal Cauchy problem, the rational reconstruction of the coordinate ratios, the contraction of exceptional curves, the transport by the partial connection and the vanishing argument, and that the example on an abelian surface times the projective line does not contradict the argument. The audit's results index lists no review of the Kähler manuscript.	Part of the completed Lattice24 audit; the reviews are published under CC BY 4.0.
2026-10-18	AI Proof Watch, record OpenAI reports compatible universal-cover splitting for Kähler manifolds	Catalogue record, assessment	Rates the importance as notable, as resolving the two-summand integrable form of Beauville's compatible splitting question, and the AI involvement as AI-led. It lists as limitations that both summands must be integrable and that automatic integrability and the other corollaries are separate from this claim. It rates the technical verification as formal, on OpenAI's reported Lean proof and Comparator statement, consistent with the scope note described under Formalization on this page, and the human understanding as few, the default when no named explanation is documented.	Curated public tracker; record published 18 October 2026, assessment reviewed 31 October 2026. Read on 1 November 2026.
2026-10-18	AI Proof Watch, record Integrability of split tangent bundles on rationally connected manifolds	Catalogue record, assessment	Rates the importance as notable, as removing the integrability premise in Höring's rationally connected projective setting, and the AI involvement as AI-led. It lists as limitations that the Lean scope covers automatic integrability, that the product corollary uses Höring's earlier theorem, and that the compact Kähler universal-cover result has different assumptions. It rates the technical verification as formal, on the source-reported Lean theorem for integrability of both summands without a local build, consistent with the scope note described under Formalization on this page, and the human understanding as few, the default when no named explanation is documented.	Curated public tracker; record published 18 October 2026, assessment reviewed 31 October 2026. Read on 1 November 2026.

Notes

• The background summarizes the manuscripts' own account of earlier work.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.