Oct 6, 2026
Lean formalization in OpenAI math repository (Result 039)
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 'Maximal Seshadri constants on arbitrary polarized surfaces'. We prove that, for every smooth integral complex projective surface S and every ample line bundle L, the multipoint Seshadri constant at r very general points equals \sqrt{L^2/r} for every sufficiently large integer r. This resolves positively the qualitative Nagata–Biran conjecture for surfaces.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 039). The Lean development was not rebuilt locally.