Oct 6, 2026
Lean formalization in OpenAI math repository (Result 052)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Universal-cover splitting for compact Kähler manifolds'. We prove the two-summand form of Beauville's compatible splitting conjecture. If the tangent bundle of a compact connected Kähler manifold decomposes into two integrable holomorphic subbundles of positive rank, then its ordinary universal cover admits a product decomposition whose factor tangent bundles are the lifted specified summands.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 052). The Lean development was not rebuilt locally.