∑math20

Algebraic and complex geometry · Result 050

A counterexample to Griffiths’ positivity conjecture

1 paperLean

Constructs ample rank-two bundles on \(\mathbb P^1\times\mathbb P^1\) with no smooth Hermitian metric of strictly Griffiths-positive curvature, disproving Griffiths' positivity conjecture already on the quadric surface.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

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

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

OpenAI · September 24, 2026

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.

Read PDF Download Source

Cite
@misc{OAI:ample-rank-two-bundles-on-the-quadric-surface-without-griffiths-positive-metrics-September-24-2026,
  author = {{OpenAI}},
  title = {{Ample rank-two bundles on the quadric surface without Griffiths-positive metrics}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/ample-rank-two-bundles-on-the-quadric-surface-without-griffiths-positive-metrics-September-24-2026/paper.pdf}{OAI:ample-rank-two-bundles-on-the-quadric-surface-without-griffiths-positive-metrics-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Griffiths' positivity conjecture predicts that every ample holomorphic vector bundle on a smooth complex projective variety admits a smooth Hermitian metric with strictly Griffiths-positive curvature. The formalized counterexample starts with a rank-two algebraic bundle \(G\) on \(\mathbb P^1\times\mathbb P^1\). Its coordinatewise power pullbacks, tensored with \(\mathcal O(1,1)\), are ample for every positive power but admit no such metric for all sufficiently large powers.

The separate very-ampleness result for all admissible even exponents is not included.

Comparator links

ResultComparator statement
Ample bundles without Griffiths-positive metricsQuadricBundles.lean

Scope note on GitHub →