Oct 6, 2026
Lean formalization in OpenAI math repository (Result 066)
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 'Uniform Cartier sections for Fano type contractions'. We prove the Cartier-divisor conjecture of Birkar and Shokurov for rational boundaries in characteristic zero and for real boundaries over ℂ. For an ϵ-lc Fano type contraction with positive-dimensional base and nef negative log canonical class, a Cartier divisor through any prescribed base point can be chosen with pullback log canonical threshold bounded below in terms of the dimension and ϵ alone.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 066). The Lean development was not rebuilt locally.