Lean formalization in OpenAI math repository (Result 047)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'An explicit failure of complex affine-space cancellation'. We construct an explicit integral complex affine fourfold X with X\times\mathbb A^1\cong\mathbb A^5 but X\not\cong\mathbb A^4. This gives a negative answer to Zariski's affine-space cancellation problem over ℂ in dimension four. The same construction disproves the Stable Coordinate Conjecture in ambient dimension five and yields smooth 𝔸3-fibrations over 𝔸1 and 𝔸2 that are not Zariski-locally trivial. These fibrations disprove the Dolgachev–Weisfeiler affine-fibration conjecture over these bases.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 047). The Lean development was not rebuilt locally.