Back to Problems
harthshorne_conjecture
Specification
There are no indecomposable vector bundles of rank 2 on $\mathbb{P}^n$ for $n \ge 7$. This is conjecture 6.3 in _VARIETIES OF SMALL CODIMENSION IN PROJECTIVE SPACE_, R. Hartshorne
Lean 4 Statement
theorem harthshorne_conjecture (n : ℕ) (hn : 7 ≤ n)
(𝓕 : VectorBundles ℙ(Fin (n + 1); Spec (.of ℂ)))
(h𝓕 : 𝓕.rank = 2) :
Nonempty (𝓕.Splitting (Fin 2))
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.