# A counterexample to Griffiths’ positivity conjecture

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

- [Ample rank-two bundles on the quadric surface without Griffiths-positive metrics](../../preprints/ample-rank-two-bundles-on-the-quadric-surface-without-griffiths-positive-metrics-September-24-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Ample bundles without Griffiths-positive metrics | [QuadricBundles.lean](../ComparatorChallenges/QuadricBundles.lean) |