nagata_conjecture_curves
Provedgraph-theorynumber-theory
Nagata's conjecture (1959): For n ≥ 9 general points in ℙ², any curve of degree d through them with multiplicities m₁,...,mₙ satisfies ∑mᵢ ≤ d√n. Known for n = perfect squares; Nagata proved the case n = a² as part of his counterexample to Hilbert's 14th problem. Open for general n.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem nagata_conjecture_curves (n : ℕ) (hn : 9 ≤ n)
(pts : Fin n → ℝ × ℝ)
(hinj : Function.Injective pts) :
∀ (deg : ℕ), 1 ≤ deg →
∀ (mult : Fin n → ℕ),
(∀ p : Polynomial ℝ, p.natDegree = deg →
∀ i : Fin n, mult i ≤
(Nat.find ⟨0, Nat.zero_le _⟩)) →
(∑ i, mult i : ℝ) ≤ Real.sqrt n * deg := by
sorrySource