Ample rank-two bundles on the quadric surface without Griffiths-positive metrics

Lean formalization in OpenAI math repository (Result 050)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Ample rank-two bundles on the quadric surface without Griffiths-positive metrics'. We give counterexamples to Griffiths' conjecture in rank two on the quadric surface \mathbb P^1\times\mathbb P^1. We construct an explicit bundle G whose coordinatewise power pullbacks, tensored with \mathcal O(1,1), are ample for every positive power, but admit no smooth strictly Griffiths-positive Hermitian metric for all sufficiently large powers.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 050). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository