Algebraic and complex geometry · Result 039

Nagata’s conjecture and maximal Seshadri constants

4 papersLean

Proves Nagata's strict inequality \(\sum_i m_i\lt d\sqrt r\) for every nonzero effective plane curve of degree d through r ≥ 10 very general complex points, with arbitrary multiplicities m_i. It also proves maximal multipoint Seshadri constants \((L^n/r)^{1/n}\) for every smooth polarized projective variety of dimension n ≥ 2 and all sufficiently large r: at very general points over ℂ, and at the geometric generic tuple over any algebraically closed field of positive characteristic.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 4

Nagata's conjecture for plane curves

OpenAI · September 23, 2026

We prove that a nonzero effective plane curve of degree d at r ≥ 10 very general complex points has total multiplicity strictly less than \(d\sqrt r\). The inequality holds simultaneously for all curves, including reducible and nonreduced curves, and establishes Nagata's conjecture in its strict, nonhomogeneous form.

Read PDF Download Source

Cite

@misc{OAI:Nagatas-Conjecture-for-Plane-Curves-September-23-2026,
  author = {{OpenAI}},
  title = {{Nagata's conjecture for plane curves}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Nagatas-Conjecture-for-Plane-Curves-September-23-2026/main.pdf}{OAI:Nagatas-Conjecture-for-Plane-Curves-September-23-2026}},
  year = {2026}
}

Maximal Seshadri constants on arbitrary polarized surfaces

OpenAI · September 23, 2026

We prove that, for every smooth integral complex projective surface S and every ample line bundle L, the multipoint Seshadri constant at r very general points equals \(\sqrt{L^2/r}\) for every sufficiently large integer r. This resolves positively the qualitative Nagata–Biran conjecture for surfaces.

Read PDF Download Source

Cite

@misc{OAI:Maximal-Seshadri-Constants-on-Arbitrary-Polarized-Surfaces-September-23-2026,
  author = {{OpenAI}},
  title = {{Maximal Seshadri constants on arbitrary polarized surfaces}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Maximal-Seshadri-Constants-on-Arbitrary-Polarized-Surfaces-September-23-2026/main.pdf}{OAI:Maximal-Seshadri-Constants-on-Arbitrary-Polarized-Surfaces-September-23-2026}},
  year = {2026}
}

Maximal Multipoint Seshadri Constants in Higher Dimensions

OpenAI · October 5, 2026

Let L be an ample line bundle on a smooth integral complex projective variety X of dimension n ≥ 3. We prove that there is a threshold \(r_0=r_0(X,L)\) such that for every integer \(r\ge r_0\), the ordinary multipoint Seshadri constant at r very general points equals the volume bound \((L^n/r)^{1/n}\). This establishes the qualitative Nagata–Biran–Szemberg assertion in these dimensions.

Read PDF Download Source

Cite

@misc{OAI:Maximal-Multipoint-Seshadri-Constants-in-Higher-Dimensions-October-5-2026,
  author = {{OpenAI}},
  title = {{Maximal Multipoint Seshadri Constants in Higher Dimensions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Maximal-Multipoint-Seshadri-Constants-in-Higher-Dimensions-October-5-2026/main.pdf}{OAI:Maximal-Multipoint-Seshadri-Constants-in-Higher-Dimensions-October-5-2026}},
  year = {2026}
}

Maximal multipoint Seshadri constants in positive characteristic

OpenAI · October 5, 2026

Let L be an ample line bundle on a smooth integral projective variety X over an algebraically closed field of positive characteristic, with \(\dim X=n\ge3\). We prove that there is a threshold \(r_0=r_0(X,L)\) such that for every integer \(r\ge r_0\), the ordinary multipoint Seshadri constant at the geometric generic tuple of r points equals the volume bound \((L^n/r)^{1/n}\). The same conclusion holds in dimension two. This establishes the positive-characteristic form of the qualitative Nagata–Biran–Szemberg assertion at geometric generic tuples.

Read PDF Download Source

Cite

@misc{OAI:Maximal-multipoint-Seshadri-constants-in-positive-characteristic-October-5-2026,
  author = {{OpenAI}},
  title = {{Maximal multipoint Seshadri constants in positive characteristic}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Maximal-multipoint-Seshadri-constants-in-positive-characteristic-October-5-2026/seshadri-positive-characteristic.pdf}{OAI:Maximal-multipoint-Seshadri-constants-in-positive-characteristic-October-5-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

Nagata's conjecture asserts that a nonzero effective plane curve of degree \(d\), with multiplicities at least \(m_i\) at \(r\ge10\) very general points, satisfies \(\sum_i m_i<d\sqrt r\).

The formalization establishes this inequality simultaneously for all curves and multiplicity vectors outside one countable union of proper Zariski-closed exceptional sets with nonempty complement. Reducible curves, repeated components, and unequal multiplicities are included, in both effective-curve and homogeneous-polynomial formulations. The formalization also includes the passage from homogeneous effective cycles to equations.

The maximality question asks whether the multipoint Seshadri constant reaches the upper bound \(\sqrt{L^2/r}\) at very general points once \(r\) is sufficiently large. The formalized result establishes this for every smooth integral complex projective surface \(S\) and ample line bundle \(L\).

For every \(r\) above a threshold depending on \((S,L)\), it gives a countable union of proper closed exceptional sets with nonempty complement. Outside it, the constant is \(\sqrt{L^2/r}\) and the boundary class defining this Seshadri constant on the point blowup is nef. The threshold is not explicit or uniform over all surfaces.

Comparator links

Result	Comparator statement
Nagata's conjecture	Nagata.lean
Eventual maximal Seshadri constants	MaximalSeshadriConstants.lean

Scope note on GitHub →