Prove QuadricBundles (openai/math family 050: A counterexample to Griffiths' positivity conjecture) in Lean…
Prove QuadricBundles (openai/math family 050: A counterexample to Griffiths' positivity conjecture) in Lean…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 050 of the release, A counterexample to Griffiths' positivity conjecture (Algebraic…
The task
Context: this statement belongs to family 050 of the release, *A counterexample to Griffiths' positivity conjecture* (Algebraic and complex geometry). The family as a whole: Constructs ample rank-two bundles on $\mathbb P^1\times\mathbb P^1$ with no smooth Hermitian metric of strictly Griffiths-positive curvature,…
Part of raising-heart/openai-math.