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

Formalization

• OpenAI math release, Lean scope notes for result 050 (release repository, lean/docs/050.md, 2026-10-06). The release's scope note says the formalization covers ampleness of all twisted power pullbacks $E_m$ and the absence of strictly Griffiths-positive metrics for large $m$, but not the separate very-ampleness result for admissible even exponents.
• OpenAI math release, QuadricBundles.lean (comparator statement) (release repository, lean/ComparatorChallenges/QuadricBundles.lean). Comparator statement SourceMainTheorem encoding Theorem 1.1 (rank-two $G$, ample power-pullback twists $E_m$, no smooth strictly Griffiths-positive Hermitian metric for $m \ge m_0$); in this file main_theorem is closed by sorry, as is usual for a comparator challenge statement.

Related prior literature mentioned by others

• Yun-Heng Du and Song-Yan Xie, Ample vector bundles without Griffiths-semipositive metrics (arXiv:2609.26504, 2026-09-22). The AI Proved What? exposition identifies this earlier claim of an ample rank-two bundle on an abelian surface without a smooth Griffiths-semipositive Hermitian metric as a different construction cited by the quadric paper.
• Kefeng Liu and Xueyuan Wan, Stable ample vector bundles without semipositive Kobayashi curvature (arXiv:2609.37309, 2026-09-29). The AI Proved What? exposition also points to this pre-release paper, cited in the manuscript, which claims slope-stable ample rank-two bundles on every Hirzebruch surface without smooth strongly pseudoconvex Finsler metrics of semipositive Kobayashi curvature.

Possibly relevant literature (found by the agent, not checked)

• C. Mourougane, S. Takayama, Hodge metrics and positivity of direct images (arXiv:math/0505324; J. reine angew. Math. 606, 2007). Gives a smooth Griffiths-positive metric on $S^kE\otimes\det E$ for ample $E$ on a projective manifold, which is relevant to the paper's discussion of positive results obtained only after modifying the bundle (Berndtsson, Liu–Sun–Yang).
• P. Naumann, An approach to Griffiths conjecture (arXiv:1710.10034, October 2017). Proposes a relative Kähler–Ricci flow approach to producing Griffiths-positive $L^2$ metrics, which bears on the paper's survey of analytic approaches (Demailly, Pingali, Murakami).
• H. Feng, K. Liu, X. Wan, Complex Finsler vector bundles with positive Kobayashi curvature (arXiv:1811.08617; accepted by Math. Res. Lett. per the arXiv comments). Proves that Kobayashi-positive Finsler bundles are ample, which is relevant to the paper's contrast between Hermitian metrics and Kobayashi's Finsler characterization and to the cited Liu–Wan preprint.
• K.-R. Wu, Positively curved Finsler metrics on vector bundles (arXiv:2107.00538, July 2021). Builds Kobayashi-positive convex Finsler metrics from Griffiths-negative $L^2$ metrics on $S^kE^*$, which bears on the paper's remark that its obstruction concerns Hermitian, not Finsler, metrics.

Digests and expositions

• AI Proved What?, Ample, not positive? A counterexample to Griffiths’ positivity conjecture (episode 050, October 2026). This video and transcript outline the graph construction, symmetric-power ampleness argument, quadratic limit and invariant-measure obstruction, while distinguishing the claimed theorem from its formalization scope and independent review. [AI-generated per source]
• Open Mathematics Courses, Griffiths positivity on the quadric (online course, 2026). Five lessons with exercises and solutions explain the paper’s construction and proof, with authorship and self-checking attributed to Claude Opus 5.5 and independent review explicitly incomplete. [AI-generated per source]