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 'Nagata's conjecture for plane curves'. We prove that a nonzero effective plane curve of degree d at r ≥ 10 very general complex points has total multiplicity strictly less than d\sqrt r. The inequality holds simultaneously for all curves, including reducible and nonreduced curves, and establishes Nagata's conjecture in its strict, nonhomogeneous form.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 039). The Lean development was not rebuilt locally.