Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Lean statement

Nagata’s conjecture

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Nagata's conjecture

Theorems selected for verification: OAI.Nagata.Workers.W30.exists_positive_degree_equation_of_homogeneous_cycle OAI.Nagata.nagata_conjecture OAI.Nagata.nagata_conjecture_coordinates

Lean statement file: Nagata.leanShow on the mapFamily 039. OpenAI lists this as a main result in its Lean catalogue.

See the candidate theoremWho ran the proof-verification programReport a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem exists_positive_degree_equation_of_homogeneous_cycle    (cycle : Ideal TernaryPolynomial →₀ ℕ) (nonzero : cycle ≠ 0)    (homogeneous : ∀ ideal ∈ cycle.support,      ideal.IsPrime ∧ ideal ≠ ⊥ ∧ ideal.IsPrincipal ∧        ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin 3) ℂ)) :    ∃ polynomial : TernaryPolynomial,      polynomial ≠ 0 ∧ polynomial.IsHomogeneous polynomial.totalDegree ∧        0 < polynomial.totalDegree ∧ equationIdealCycle polynomial = cycle := by  sorrydef FullNagata : Prop :=  ∀ count : ℕ, 10 ≤ count →    ∃ exceptional : ℕ → Set (OrderedDistinctPoints count),      (∀ index, IsConfigurationZariskiClosed (exceptional index) ∧        exceptional index ≠ Set.univ) ∧      (∃ points : OrderedDistinctPoints count, ∀ index, points ∉ exceptional index) ∧      ∀ points : OrderedDistinctPoints count, (∀ index, points ∉ exceptional index) →        ∀ degree : ℕ, 1 ≤ degree →        ∀ polynomial : MvPolynomial (Fin 3) ℂ,          polynomial ≠ 0 → polynomial.IsHomogeneous degree →        ∀ multiplicities : Fin count → ℕ,          (∀ index, multiplicityAtLeast polynomial (points.val index) (multiplicities index)) →          (∑ index, (multiplicities index : ℝ)) < (degree : ℝ) * Real.sqrt (count : ℝ)theorem nagata_conjecture :    ∀ count : ℕ, 10 ≤ count →      ∃ exceptional : ℕ → Set (OrderedDistinctPoints count),        (∀ index, IsConfigurationZariskiClosed (exceptional index) ∧          exceptional index ≠ Set.univ) ∧        (∃ points : OrderedDistinctPoints count, ∀ index, points ∉ exceptional index) ∧        ∀ points : OrderedDistinctPoints count, (∀ index, points ∉ exceptional index) →          ∀ curve : Workers.W10.EffectivePlaneCurve, ∀ multiplicities : Fin count → ℕ,            (∀ index, multiplicities index ≤ W15.curveOrdinaryMultiplicity curve (points.val index)) →            (∑ index, (multiplicities index : ℝ)) <              (Workers.W10.curveDegree curve : ℝ) * Real.sqrt (count : ℝ) := by  sorrytheorem nagata_conjecture_coordinates : FullNagata := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

  • definition OAI.Nagata.AffineMultiplicity.pointIdeal line 42

    def pointIdeal (point : σ → K) : Ideal (MvPolynomial σ K) :=  RingHom.ker (MvPolynomial.eval point)

  • definition OAI.Nagata.AffineMultiplicity.orderAtLeast line 45

    def orderAtLeast (point : σ → K) (multiplicity : ℕ)    (polynomial : MvPolynomial σ K) : Prop :=  polynomial ∈ pointIdeal point ^ multiplicity

  • definition OAI.Nagata.AffineMultiplicity.translateHom line 49

    def translateHom (point : σ → K) : MvPolynomial σ K →+* MvPolynomial σ K :=  MvPolynomial.eval₂Hom MvPolynomial.C    (fun index => MvPolynomial.X index + MvPolynomial.C (point index))

  • definition OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity line 92

    def ordinaryMultiplicity (point : σ → K) (polynomial : MvPolynomial σ K)    (nonzero : polynomial ≠ 0) : ℕ :=  (translateHom point polynomial).support.inf'    (translated_support_nonempty point polynomial nonzero) Finsupp.degree

  • abbreviation OAI.Nagata.ProjectiveGeometry.PlanePoint line 101

    abbrev PlanePoint := Projectivization ℂ (Fin 3 → ℂ)

  • abbreviation OAI.Nagata.ProjectiveGeometry.OrderedDistinctPoints line 103

    abbrev OrderedDistinctPoints (count : ℕ) :=  {points : Fin count → PlanePoint // Function.Injective points}

  • structure OAI.Nagata.ProjectiveGeometry.MultihomogeneousEquation line 106

    structure MultihomogeneousEquation (count : ℕ) where  polynomial : MvPolynomial (Fin count × Fin 3) ℂ  multidegree : Fin count → ℕ  homogeneous : ∀ exponent ∈ polynomial.support, ∀ index,    (∑ coordinate : Fin 3, exponent (index, coordinate)) = multidegree index

  • definition OAI.Nagata.ProjectiveGeometry.equationVanishes line 112

    def equationVanishes {count : ℕ} (equation : MultihomogeneousEquation count)    (points : Fin count → PlanePoint) : Prop :=  ∀ (vectors : Fin count → Fin 3 → ℂ) (nonzero : ∀ index, vectors index ≠ 0),    (∀ index, Projectivization.mk ℂ (vectors index) (nonzero index) = points index) →    MvPolynomial.eval (fun index => vectors index.1 index.2) equation.polynomial = 0

  • definition OAI.Nagata.ProjectiveGeometry.IsProductZariskiClosed line 118

    def IsProductZariskiClosed {count : ℕ} (locus : Set (Fin count → PlanePoint)) : Prop :=  ∃ equations : Set (MultihomogeneousEquation count),    ∀ points, points ∈ locus ↔ ∀ equation ∈ equations, equationVanishes equation points

  • definition OAI.Nagata.ProjectiveGeometry.IsConfigurationZariskiClosed line 122

    def IsConfigurationZariskiClosed {count : ℕ}    (locus : Set (OrderedDistinctPoints count)) : Prop :=  ∃ ambient : Set (Fin count → PlanePoint), IsProductZariskiClosed ambient ∧    ∀ points, points ∈ locus ↔ points.val ∈ ambient

  • abbreviation OAI.Nagata.ProjectiveGeometry.ChartVariables line 127

    abbrev ChartVariables (chart : Fin 3) := {coordinate : Fin 3 // coordinate ≠ chart}

  • definition OAI.Nagata.ProjectiveGeometry.dehomogenize line 129

    def dehomogenize (chart : Fin 3) (polynomial : MvPolynomial (Fin 3) ℂ) :    MvPolynomial (ChartVariables chart) ℂ :=  MvPolynomial.eval₂ MvPolynomial.C    (fun coordinate => if equal : coordinate = chart then 1      else MvPolynomial.X ⟨coordinate, equal⟩) polynomial

  • definition OAI.Nagata.ProjectiveGeometry.chartCoordinates line 135

    def chartCoordinates (chart : Fin 3) (point : PlanePoint) : ChartVariables chart → ℂ :=  fun coordinate => point.rep coordinate.val / point.rep chart

  • definition OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast line 139

    def multiplicityAtLeast (polynomial : MvPolynomial (Fin 3) ℂ)    (point : PlanePoint) (multiplicity : ℕ) : Prop :=  ∀ chart : Fin 3, point.rep chart ≠ 0 →    AffineMultiplicity.orderAtLeast (chartCoordinates chart point) multiplicity      (dehomogenize chart polynomial)

  • abbreviation OAI.Nagata.Workers.W30.TernaryPolynomial line 157

    abbrev TernaryPolynomial := MvPolynomial (Fin 3) ℂ

  • definition OAI.Nagata.Workers.W30.equationMultiplicity line 161

    def equationMultiplicity (polynomial : TernaryPolynomial) :    Associates TernaryPolynomial →₀ ℕ :=  factorization (Associates.mk polynomial)

  • definition OAI.Nagata.Workers.W30.associatePrincipalIdeal line 165

    def associatePrincipalIdeal (associate : Associates TernaryPolynomial) :    Ideal TernaryPolynomial :=  (Ideal.associatesEquivIsPrincipal TernaryPolynomial associate).val

  • definition OAI.Nagata.Workers.W30.equationIdealCycle line 169

    def equationIdealCycle (polynomial : TernaryPolynomial) : Ideal TernaryPolynomial →₀ ℕ :=  (equationMultiplicity polynomial).mapDomain associatePrincipalIdeal

  • abbreviation OAI.Nagata.W16.PlanePolynomial line 188

    abbrev PlanePolynomial := MvPolynomial (Fin 3) ℂ

  • structure OAI.Nagata.W16.NonzeroHomogeneousForm line 190

    structure NonzeroHomogeneousForm (degree : ℕ) where  polynomial : PlanePolynomial  homogeneous : polynomial.IsHomogeneous degree  nonzero : polynomial ≠ 0

  • definition OAI.Nagata.Workers.W10.EffectivePlaneCurve line 283

    def EffectivePlaneCurve := {cycle : Ideal TernaryPolynomial →₀ ℕ //  cycle ≠ 0 ∧ ∀ ideal ∈ cycle.support,    ideal.IsPrime ∧ ideal ≠ ⊥ ∧ ideal.IsPrincipal ∧      ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin 3) ℂ)}

  • definition OAI.Nagata.Workers.W10.curveEquation line 289

    def curveEquation (curve : EffectivePlaneCurve) : TernaryPolynomial :=  Classical.choose (exists_positive_degree_equation_of_homogeneous_cycle    curve.val curve.property.1 curve.property.2)

  • definition OAI.Nagata.Workers.W10.curveDegree line 303

    def curveDegree (curve : EffectivePlaneCurve) : ℕ := (curveEquation curve).totalDegree

  • definition OAI.Nagata.Workers.W10.curveForm line 309

    def curveForm (curve : EffectivePlaneCurve) : NonzeroHomogeneousForm (curveDegree curve) :=  ⟨curveEquation curve, curveEquation_homogeneous curve, curveEquation_nonzero curve⟩

2 more definitions are reached the same way; the full file lists them.

Possible paper match, with no recorded review

Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.

Words of the Lean statement, its names split into words, that also appear in the theorem: effective, plane, curve, zariski, nonzero, nonempty, countable, degree and three more. Found in the paper’s title, which its main theorem states: conjecture and nagatas. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: complement, union and proper.

Statements in Nagata’s conjecture for plane curves come first because the release’s name for this Lean statement shares words with that paper’s title.

Theorem 1.1 of Nagata’s conjecture for plane curves

Theorem

For every integer r\ge10, there is a countable union E_r of proper Zariski-closed subsets of U_r, with nonempty complement, such that the following holds for every tuple (p_1,\ldots,p_r)\notin E_r. If C is a nonzero effective plane curve of degree d\ge1 and m_1,\ldots,m_r\in\Z_{\ge0} satisfy \mult_{p_i}C\ge m_i, then

d\sqrt r>\sum_{i=1}^r m_i.
Section 1, Introduction Read it in the paper TeX source, line 31
Show the TeX
For every integer $r\ge10$, there is a countable union $E_r$ of proper
Zariski-closed subsets of $U_r$, with nonempty complement, such that the
following holds for every tuple $(p_1,\ldots,p_r)\notin E_r$.
If $C$ is a nonzero effective plane curve of degree $d\ge1$ and
$m_1,\ldots,m_r\in\Z_{\ge0}$ satisfy $\mult_{p_i}C\ge m_i$, then
\[
 d\sqrt r>\sum_{i=1}^r m_i.
\]

Other possible paper matches, closest wording first

  • Corollary 6.1 of Nagata’s conjecture for plane curves. Words of the Lean statement, its names split into words, that also appear in the theorem: zero, multiplicity, zariski, nonempty, countable, degree and three more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: outside, complement, union and proper.
  • Proposition 2.2 of Nagata’s conjecture for plane curves. Words of the Lean statement, its names split into words, that also appear in the theorem: polynomial, coefficients, vectors, least, multiplicity, nonzero and two more.
  • Proposition 5.3 of Maximal Seshadri constants on arbitrary polarized surfaces. Words of the Lean statement, its names split into words, that also appear in the theorem: vanishes, exceptional, homogeneous, curves, real, least and nine more.
  • Proposition 3.1 of Nagata’s conjecture for plane curves. Words of the Lean statement, its names split into words, that also appear in the theorem: scalar, coordinate, least, multiplicity, choose, nonzero and two more.
  • Theorem 1.1 of Maximal Seshadri constants on arbitrary polarized surfaces. Words of the Lean statement, its names split into words, that also appear in the theorem: property, zariski, nonempty, complex, countable, sqrt and three more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: complement, union and proper.
  • Corollary 5.5 of Maximal Seshadri constants on arbitrary polarized surfaces. Words of the Lean statement, its names split into words, that also appear in the theorem: zero, zariski, nonempty, countable, sqrt, projective and two more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: outside, one, complement, union and proper.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

  • Accepted Their term: “CERTIFIED”.

    Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.

    Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

  • Accepted Their term: “comparator-sandboxed-pass”.

    Re-run through Comparator in a sandboxed virtual machine: accepted.

    Reported 8 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 039’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

  • MathVet

    Finds part of it stated, or a narrower or weaker statement Their term: “partial”.

    Only a special case is stated, or a co-equal headline claim has no challenge statement. Their record

    Their note: Nagata (r >= 10, very general, arbitrary multiplicities) fully stated; maximal multipoint Seshadri constants only for smooth projective surfaces over C, not (L^n/r)^{1/n} in dimension n >= 2 and not over algebraically closed fields of positive characteristic.

    Definitions the group asks readers to compare with the paper: Seshadri side is custom scheme theory: selfIntersection S L := χ(L^2) - 2χ(L) + χ(O) (= L^2 by Riemann-Roch, checked), curveDegree := χ(L|_C) - χ(O_C), cohomology := Abelian.Ext (structureSheaf X) M n with cohomologyDimension := Module.finrank ℂ (junk 0 if infinite-dimensional), IsBlowup by universal property, curveMultiplicity via idealOrder of the stalk kernel; Nagata side defines the curve equation by Classical.choose of a sorry'd existence theorem (curveEquation) that is itself a checked theorem_name

  • Carlos Toledo’s cert-machine

    Finds part of it stated, or a narrower or weaker statement Their term: “NARROWER — UNLINKED”.

    The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link. Their record

    Their note: maximal multipoint Seshadri constants in dimension n >= 3 (complex, very general points) and in positive characteristic (all n >= 2, geometric generic tuple) are claimed by the headline but not stated; Lean states only smooth complex projective surfaces

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“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.”

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

372 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 124 to its own declarations, 148 to Mathlib’s documentation. 20 declared names also link to the same declaration in OpenAI’s library. 1 identifier stays plain because it resolves to no single declaration: a variable Lean binds automatically, notation, or a name the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlib.Algebra.CharZero.Infiniteimport Mathlib.Algebra.Group.Irreducible.Defsimport Mathlib.Algebra.MvPolynomial.Evalimport Mathlib.Algebra.MvPolynomial.NoZeroDivisorsimport Mathlib.Algebra.MvPolynomial.Renameimport Mathlib.Analysis.Real.Sqrtimport Mathlib.Basic.Complex.Basicimport Mathlib.Data.Fin.SuccPredimport Mathlib.Data.Fin.Tuple.Basicimport Mathlib.Data.Fintype.BigOperatorsimport Mathlib.LinearAlgebra.Projectivization.Basicimport Mathlib.RingTheory.GradedAlgebra.Homogeneous.Idealimport Mathlib.RingTheory.Ideal.Heightimport Mathlib.RingTheory.Ideal.IsPrincipalimport Mathlib.RingTheory.Ideal.Mapsimport Mathlib.RingTheory.Ideal.Maximalimport Mathlib.RingTheory.Localization.AtPrime.Basicimport Mathlib.RingTheory.MvPolynomial.Homogeneousimport Mathlib.RingTheory.MvPolynomial.Idealimport Mathlib.RingTheory.Polynomial.UniqueFactorizationimport Mathlib.RingTheory.UniqueFactorizationDomain.Basicimport Mathlib.RingTheory.UniqueFactorizationDomain.Finsuppnamespace OAI/-!# Nagata's strict inequality for very general complex plane configurationsThe exceptional family is chosen before every curve and multiplicity vector.Closedness means common multihomogeneous zero loci on the product of projectiveplanes, restricted to the open set of ordered distinct configurations.-/noncomputable sectionopen scoped BigOperatorsnamespace Nagata.AffineMultiplicityvariable {σ K : Type*} [CommRing K]def pointIdeal (point : σ → K) : Ideal (MvPolynomial σ K) :=  RingHom.ker (MvPolynomial.eval point)def orderAtLeast (point : σ → K) (multiplicity : ℕ)    (polynomial : MvPolynomial σ K) : Prop :=  polynomial ∈ pointIdeal point ^ multiplicitydef translateHom (point : σ → K) : MvPolynomial σ K →+* MvPolynomial σ K :=  MvPolynomial.eval₂Hom MvPolynomial.C    (fun index => MvPolynomial.X index + MvPolynomial.C (point index))@[simp] theorem translateHom_C (point : σ → K) (coefficient : K) :    translateHom point (MvPolynomial.C coefficient) = MvPolynomial.C coefficient := by  simp [translateHom]@[simp] theorem translateHom_X (point : σ → K) (index : σ) :    translateHom point (MvPolynomial.X index) = MvPolynomial.X index + MvPolynomial.C (point index) := by  simp [translateHom]theorem translateHom_neg_comp (point : σ → K) :    (translateHom (-point)).comp (translateHom point) = RingHom.id _ := by  apply MvPolynomial.ringHom_ext  · intro coefficient; simp  · intro index; simp [add_assoc]theorem translateHom_comp_neg (point : σ → K) :    (translateHom point).comp (translateHom (-point)) = RingHom.id _ := by  simpa only [neg_neg] using translateHom_neg_comp (-point)def translateEquiv (point : σ → K) : MvPolynomial σ K ≃+* MvPolynomial σ K :=  { translateHom point with    invFun := translateHom (-point)    left_inv := fun polynomial => RingHom.congr_fun (translateHom_neg_comp point) polynomial    right_inv := fun polynomial => RingHom.congr_fun (translateHom_comp_neg point) polynomial }@[simp] theorem translateEquiv_apply (point : σ → K) (polynomial : MvPolynomial σ K) :    translateEquiv point polynomial = translateHom point polynomial := rfltheorem translate_ne_zero (point : σ → K) (polynomial : MvPolynomial σ K)    (nonzero : polynomial ≠ 0) : translateHom point polynomial ≠ 0 := by  intro translated_zero  apply nonzero  apply (translateEquiv point).injective  simpa only [translateEquiv_apply, map_zero] using translated_zerotheorem translated_support_nonempty (point : σ → K) (polynomial : MvPolynomial σ K)    (nonzero : polynomial ≠ 0) : (translateHom point polynomial).support.Nonempty :=  MvPolynomial.support_nonempty.mpr (translate_ne_zero point polynomial nonzero)/-- The least total degree of a nonzero Taylor coefficient. -/def ordinaryMultiplicity (point : σ → K) (polynomial : MvPolynomial σ K)    (nonzero : polynomial ≠ 0) : ℕ :=  (translateHom point polynomial).support.inf'    (translated_support_nonempty point polynomial nonzero) Finsupp.degreeend Nagata.AffineMultiplicitynamespace Nagata.ProjectiveGeometryabbrev PlanePoint := Projectivization ℂ (Fin 3 → ℂ)abbrev OrderedDistinctPoints (count : ℕ) :=  {points : Fin count → PlanePoint // Function.Injective points}structure MultihomogeneousEquation (count : ℕ) where  polynomial : MvPolynomial (Fin count × Fin 3) ℂ  multidegree : Fin count → ℕ  homogeneous : ∀ exponent ∈ polynomial.support, ∀ index,    (∑ coordinate : Fin 3, exponent (index, coordinate)) = multidegree indexdef equationVanishes {count : ℕ} (equation : MultihomogeneousEquation count)    (points : Fin count → PlanePoint) : Prop :=  ∀ (vectors : Fin count → Fin 3 → ℂ) (nonzero : ∀ index, vectors index ≠ 0),    (∀ index, Projectivization.mk ℂ (vectors index) (nonzero index) = points index) →    MvPolynomial.eval (fun index => vectors index.1 index.2) equation.polynomial = 0def IsProductZariskiClosed {count : ℕ} (locus : Set (Fin count → PlanePoint)) : Prop :=  ∃ equations : Set (MultihomogeneousEquation count),    ∀ points, points ∈ locus ↔ ∀ equation ∈ equations, equationVanishes equation pointsdef IsConfigurationZariskiClosed {count : ℕ}    (locus : Set (OrderedDistinctPoints count)) : Prop :=  ∃ ambient : Set (Fin count → PlanePoint), IsProductZariskiClosed ambient ∧    ∀ points, points ∈ locus ↔ points.val ∈ ambientabbrev ChartVariables (chart : Fin 3) := {coordinate : Fin 3 // coordinate ≠ chart}def dehomogenize (chart : Fin 3) (polynomial : MvPolynomial (Fin 3) ℂ) :    MvPolynomial (ChartVariables chart) ℂ :=  MvPolynomial.eval₂ MvPolynomial.C    (fun coordinate => if equal : coordinate = chart then 1      else MvPolynomial.X ⟨coordinate, equal⟩) polynomialdef chartCoordinates (chart : Fin 3) (point : PlanePoint) : ChartVariables chart → ℂ :=  fun coordinate => point.rep coordinate.val / point.rep chart/-- Local multiplicity lower bounds are membership in powers of the point ideal. -/def multiplicityAtLeast (polynomial : MvPolynomial (Fin 3) ℂ)    (point : PlanePoint) (multiplicity : ℕ) : Prop :=  ∀ chart : Fin 3, point.rep chart ≠ 0 →    AffineMultiplicity.orderAtLeast (chartCoordinates chart point) multiplicity      (dehomogenize chart polynomial)theorem chart_exists (point : PlanePoint) : ∃ chart : Fin 3, point.rep chart ≠ 0 := by  by_contra absent  apply point.rep_nonzero  funext chart  exact Classical.not_not.mp (fun nonzero => absent ⟨chart, nonzero⟩)end Nagata.ProjectiveGeometrynamespace Nagata.Workers.W30open UniqueFactorizationMonoidabbrev TernaryPolynomial := MvPolynomial (Fin 3) ℂlocal instance : DecidableEq (Associates TernaryPolynomial) := Classical.decEq _def equationMultiplicity (polynomial : TernaryPolynomial) :    Associates TernaryPolynomial →₀ ℕ :=  factorization (Associates.mk polynomial)def associatePrincipalIdeal (associate : Associates TernaryPolynomial) :    Ideal TernaryPolynomial :=  (Ideal.associatesEquivIsPrincipal TernaryPolynomial associate).valdef equationIdealCycle (polynomial : TernaryPolynomial) : Ideal TernaryPolynomial →₀ ℕ :=  (equationMultiplicity polynomial).mapDomain associatePrincipalIdealattribute [local instance] MvPolynomial.gradedAlgebratheorem exists_positive_degree_equation_of_homogeneous_cycle    (cycle : Ideal TernaryPolynomial →₀ ℕ) (nonzero : cycle ≠ 0)    (homogeneous : ∀ ideal ∈ cycle.support,      ideal.IsPrime ∧ ideal ≠ ⊥ ∧ ideal.IsPrincipal ∧        ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin 3) ℂ)) :    ∃ polynomial : TernaryPolynomial,      polynomial ≠ 0 ∧ polynomial.IsHomogeneous polynomial.totalDegree ∧        0 < polynomial.totalDegree ∧ equationIdealCycle polynomial = cycle := by  sorryend Nagata.Workers.W30namespace Nagata.W16abbrev PlanePolynomial := MvPolynomial (Fin 3) ℂstructure NonzeroHomogeneousForm (degree : ℕ) where  polynomial : PlanePolynomial  homogeneous : polynomial.IsHomogeneous degree  nonzero : polynomial ≠ 0theorem homogeneous_eval_scale {Variables Coefficient : Type*} [CommSemiring Coefficient]    {polynomial : MvPolynomial Variables Coefficient} {degree : ℕ}    (homogeneous : polynomial.IsHomogeneous degree)    (coordinates : Variables → Coefficient) (scalar : Coefficient) :    MvPolynomial.eval (fun index => scalar * coordinates index) polynomial =      scalar ^ degree * MvPolynomial.eval coordinates polynomial := by  classical  simp only [MvPolynomial.eval_eq, Finset.mul_sum]  apply Finset.sum_congr rfl  intro exponent supported  simp only [mul_pow, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum]  rw [← homogeneous.degree_eq_sum_deg_support supported]  ac_rflopen Nagata.ProjectiveGeometrytheorem eval_dehomogenize (chart : Fin 3) (polynomial : PlanePolynomial)    (coordinates : ChartVariables chart → ℂ) :    MvPolynomial.eval coordinates (dehomogenize chart polynomial) =      MvPolynomial.eval        (fun index => if equal : index = chart then 1 else coordinates ⟨index, equal⟩)        polynomial := by  classical  unfold dehomogenize  rw [← MvPolynomial.eval_assoc]  apply congrArg (fun values : Fin 3 → ℂ => MvPolynomial.eval values polynomial)  funext index  by_cases equal : index = chart <;> simp [equal, Function.comp_apply]theorem eval_dehomogenize_normalized {degree : ℕ} {polynomial : PlanePolynomial}    (homogeneous : polynomial.IsHomogeneous degree) (chart : Fin 3)    (coordinates : Fin 3 → ℂ) (chart_nonzero : coordinates chart ≠ 0) :    MvPolynomial.eval (fun index : ChartVariables chart => coordinates index.val / coordinates chart)        (dehomogenize chart polynomial) =      (coordinates chart)⁻¹ ^ degree * MvPolynomial.eval coordinates polynomial := by  classical  rw [eval_dehomogenize]  have normalized :      (fun index : Fin 3 => if equal : index = chart then (1 : ℂ)        else coordinates index / coordinates chart) =        fun index => (coordinates chart)⁻¹ * coordinates index := by    funext index    by_cases equal : index = chart    · subst index      simp [chart_nonzero]    · simp [equal, div_eq_mul_inv, mul_comm]  rw [normalized]  exact homogeneous_eval_scale homogeneous coordinates (coordinates chart)⁻¹theorem eval_eq_zero_of_dehomogenize_eq_zero {degree : ℕ} {polynomial : PlanePolynomial}    (homogeneous : polynomial.IsHomogeneous degree) (chart : Fin 3)    (chart_zero : dehomogenize chart polynomial = 0)    (coordinates : Fin 3 → ℂ) (chart_nonzero : coordinates chart ≠ 0) :    MvPolynomial.eval coordinates polynomial = 0 := by  have evaluated := congrArg    (MvPolynomial.eval (fun index : ChartVariables chart => coordinates index.val / coordinates chart))    chart_zero  rw [eval_dehomogenize_normalized homogeneous chart coordinates chart_nonzero, map_zero] at evaluated  exact (mul_eq_zero.mp evaluated).resolve_left (pow_ne_zero degree (inv_ne_zero chart_nonzero))theorem eq_zero_of_dehomogenize_eq_zero {degree : ℕ} {polynomial : PlanePolynomial}    (homogeneous : polynomial.IsHomogeneous degree) (chart : Fin 3)    (chart_zero : dehomogenize chart polynomial = 0) : polynomial = 0 := by  have multiplied : MvPolynomial.X chart * polynomial = 0 := by    apply ((MvPolynomial.isHomogeneous_X ℂ chart).mul homogeneous).eq_zero_of_forall_eval_eq_zero    intro coordinates    rw [MvPolynomial.eval_mul, MvPolynomial.eval_X]    by_cases chart_nonzero : coordinates chart = 0    · simp [chart_nonzero]    · rw [eval_eq_zero_of_dehomogenize_eq_zero homogeneous chart chart_zero coordinates chart_nonzero,          mul_zero]  exact (mul_eq_zero.mp multiplied).resolve_left (MvPolynomial.X_ne_zero chart)theorem dehomogenize_ne_zero {degree : ℕ} {polynomial : PlanePolynomial}    (homogeneous : polynomial.IsHomogeneous degree) (nonzero : polynomial ≠ 0)    (chart : Fin 3) : ProjectiveGeometry.dehomogenize chart polynomial ≠ 0 := by  intro chart_zero  exact nonzero (eq_zero_of_dehomogenize_eq_zero homogeneous chart chart_zero)end Nagata.W16namespace Nagata.Workers.W10open Nagata.Workers.W30 Nagata.W16attribute [local instance] MvPolynomial.gradedAlgebra/-- Nonzero finite cycles of homogeneous prime plane ideals, with natural weights. -/def EffectivePlaneCurve := {cycle : Ideal TernaryPolynomial →₀ ℕ //  cycle ≠ 0 ∧ ∀ ideal ∈ cycle.support,    ideal.IsPrime ∧ ideal ≠ ⊥ ∧ ideal.IsPrincipal ∧      ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin 3) ℂ)}/-- An equation realizing the entire cycle, including repeated components. -/def curveEquation (curve : EffectivePlaneCurve) : TernaryPolynomial :=  Classical.choose (exists_positive_degree_equation_of_homogeneous_cycle    curve.val curve.property.1 curve.property.2)theorem curveEquation_spec (curve : EffectivePlaneCurve) :    curveEquation curve ≠ 0 ∧      (curveEquation curve).IsHomogeneous (curveEquation curve).totalDegree ∧      0 < (curveEquation curve).totalDegree ∧ equationIdealCycle (curveEquation curve) = curve.val :=  Classical.choose_spec (exists_positive_degree_equation_of_homogeneous_cycle    curve.val curve.property.1 curve.property.2)theorem curveEquation_nonzero (curve : EffectivePlaneCurve) : curveEquation curve ≠ 0 :=  (curveEquation_spec curve).1def curveDegree (curve : EffectivePlaneCurve) : ℕ := (curveEquation curve).totalDegreetheorem curveEquation_homogeneous (curve : EffectivePlaneCurve) :    (curveEquation curve).IsHomogeneous (curveDegree curve) :=  (curveEquation_spec curve).2.1def curveForm (curve : EffectivePlaneCurve) : NonzeroHomogeneousForm (curveDegree curve) :=  ⟨curveEquation curve, curveEquation_homogeneous curve, curveEquation_nonzero curve⟩end Nagata.Workers.W10namespace Nagata.ProjectiveGeometrydef formOrdinaryMultiplicity {degree : ℕ} (form : W16.NonzeroHomogeneousForm degree)    (point : PlanePoint) : ℕ :=  let chart := Classical.choose (chart_exists point)  AffineMultiplicity.ordinaryMultiplicity (chartCoordinates chart point)    (dehomogenize chart form.polynomial)    (W16.dehomogenize_ne_zero form.homogeneous form.nonzero chart)end Nagata.ProjectiveGeometrynamespace Nagata.W15open Nagata.Workers.W10 Nagata.ProjectiveGeometrydef curveOrdinaryMultiplicity (curve : EffectivePlaneCurve) (point : PlanePoint) : ℕ :=  formOrdinaryMultiplicity (curveForm curve) pointend Nagata.W15namespace Nagataopen ProjectiveGeometrydef FullNagata : Prop :=  ∀ count : ℕ, 10 ≤ count →    ∃ exceptional : ℕ → Set (OrderedDistinctPoints count),      (∀ index, IsConfigurationZariskiClosed (exceptional index) ∧        exceptional index ≠ Set.univ) ∧      (∃ points : OrderedDistinctPoints count, ∀ index, points ∉ exceptional index) ∧      ∀ points : OrderedDistinctPoints count, (∀ index, points ∉ exceptional index) →        ∀ degree : ℕ, 1 ≤ degree →        ∀ polynomial : MvPolynomial (Fin 3) ℂ,          polynomial ≠ 0 → polynomial.IsHomogeneous degree →        ∀ multiplicities : Fin count → ℕ,          (∀ index, multiplicityAtLeast polynomial (points.val index) (multiplicities index)) →          (∑ index, (multiplicities index : ℝ)) < (degree : ℝ) * Real.sqrt (count : ℝ)theorem nagata_conjecture :    ∀ count : ℕ, 10 ≤ count →      ∃ exceptional : ℕ → Set (OrderedDistinctPoints count),        (∀ index, IsConfigurationZariskiClosed (exceptional index) ∧          exceptional index ≠ Set.univ) ∧        (∃ points : OrderedDistinctPoints count, ∀ index, points ∉ exceptional index) ∧        ∀ points : OrderedDistinctPoints count, (∀ index, points ∉ exceptional index) →          ∀ curve : Workers.W10.EffectivePlaneCurve, ∀ multiplicities : Fin count → ℕ,            (∀ index, multiplicities index ≤ W15.curveOrdinaryMultiplicity curve (points.val index)) →            (∑ index, (multiplicities index : ℝ)) <              (Workers.W10.curveDegree curve : ℝ) * Real.sqrt (count : ℝ) := by  sorrytheorem nagata_conjecture_coordinates : FullNagata := by  sorryend Nagataendend OAI
Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Nagata’s conjecture for plane curves

Theorem

For every integer r\ge10, there is a countable union E_r of proper Zariski-closed subsets of U_r, with nonempty complement, such that the following holds for every tuple (p_1,\ldots,p_r)\notin E_r. If C is a nonzero effective plane curve of degree d\ge1 and m_1,\ldots,m_r\in\Z_{\ge0} satisfy \mult_{p_i}C\ge m_i, then

d\sqrt r>\sum_{i=1}^r m_i.
Section 1, Introduction Read it in the paper TeX source, line 31
Show the TeX
For every integer $r\ge10$, there is a countable union $E_r$ of proper
Zariski-closed subsets of $U_r$, with nonempty complement, such that the
following holds for every tuple $(p_1,\ldots,p_r)\notin E_r$.
If $C$ is a nonzero effective plane curve of degree $d\ge1$ and
$m_1,\ldots,m_r\in\Z_{\ge0}$ satisfy $\mult_{p_i}C\ge m_i$, then
\[
 d\sqrt r>\sum_{i=1}^r m_i.
\]

Maximal Seshadri constants on arbitrary polarized surfaces

Theorem

For every smooth integral complex projective surface S and every ample line bundle L on S, there is an integer r_0=r_0(S,L) with the following property. For each integer r\ge r_0, there is a countable union Z_r of proper Zariski-closed subsets of U_r, with nonempty complement, such that for every \mathbf p\in U_r\setminus Z_r the class

\pi^*L-\sqrt{\frac{L^2}{r}}\sum_{i=1}^r E_i

is nef on the blow-up at \mathbf p. Consequently,

\varepsilon(S,L;\mathbf p)=\sqrt{\frac{L^2}{r}}.
Section 1, Introduction Read it in the paper TeX source, line 31
Show the TeX
For every smooth integral complex projective surface $S$ and every ample
line bundle $L$ on $S$, there is an integer $r_0=r_0(S,L)$ with the following
property. For each integer $r\ge r_0$, there is a countable union
$Z_r$ of proper Zariski-closed subsets of $U_r$, with nonempty complement,
such that for every $\mathbf p\in U_r\setminus Z_r$ the class
\[
 \pi^*L-\sqrt{\frac{L^2}{r}}\sum_{i=1}^r E_i
\]
is nef on the blow-up at $\mathbf p$. Consequently,
\[
 \varepsilon(S,L;\mathbf p)=\sqrt{\frac{L^2}{r}}.
\]
Configuration and file facts
OpenAI’s Lean catalogue
OpenAI lists this as a main result in its Lean catalogue.
Allowed axioms
propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports
Mathlib.Algebra.CharZero.Infinite, Mathlib.Algebra.Group.Irreducible.Defs, Mathlib.Algebra.MvPolynomial.Eval, Mathlib.Algebra.MvPolynomial.NoZeroDivisors, Mathlib.Algebra.MvPolynomial.Rename, Mathlib.Analysis.Real.Sqrt, Mathlib.Basic.Complex.Basic, Mathlib.Data.Fin.SuccPred, Mathlib.Data.Fin.Tuple.Basic, Mathlib.Data.Fintype.BigOperators, Mathlib.LinearAlgebra.Projectivization.Basic, Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal, Mathlib.RingTheory.Ideal.Height, Mathlib.RingTheory.Ideal.IsPrincipal, Mathlib.RingTheory.Ideal.Maps, Mathlib.RingTheory.Ideal.Maximal, Mathlib.RingTheory.Localization.AtPrime.Basic, Mathlib.RingTheory.MvPolynomial.Homogeneous, Mathlib.RingTheory.MvPolynomial.Ideal, Mathlib.RingTheory.Polynomial.UniqueFactorization, Mathlib.RingTheory.UniqueFactorizationDomain.Basic, Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Imports from outside Mathlib
None
Local vocabulary
29 local vocabulary declarations
Lines of Lean, without comments or blank lines
233
Second proof-verification program (nanoda)
Off in OpenAI's configuration.

Statement comparison

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas

Nagata's conjecture

Family 039: Nagata’s conjecture and maximal Seshadri constants

Candidate pairing

Theorem

For every integer r\ge10, there is a countable union E_r of proper Zariski-closed subsets of U_r, with nonempty complement, such that the following holds for every tuple (p_1,\ldots,p_r)\notin E_r. If C is a nonzero effective plane curve of degree d\ge1 and m_1,\ldots,m_r\in\Z_{\ge0} satisfy \mult_{p_i}C\ge m_i, then

d\sqrt r>\sum_{i=1}^r m_i.

Nagata’s conjecture for plane curves

TeX label thm:main, build/sections/introduction.tex, line 31

The Lean statement says

theorem exists_positive_degree_equation_of_homogeneous_cycle    (cycle : Ideal TernaryPolynomial →₀ ℕ) (nonzero : cycle ≠ 0)    (homogeneous : ∀ ideal ∈ cycle.support,      ideal.IsPrime ∧ ideal ≠ ⊥ ∧ ideal.IsPrincipal ∧        ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin 3) ℂ)) :    ∃ polynomial : TernaryPolynomial,      polynomial ≠ 0 ∧ polynomial.IsHomogeneous polynomial.totalDegree ∧        0 < polynomial.totalDegree ∧ equationIdealCycle polynomial = cycle := by  sorrydef FullNagata : Prop :=  ∀ count : ℕ, 10 ≤ count →    ∃ exceptional : ℕ → Set (OrderedDistinctPoints count),      (∀ index, IsConfigurationZariskiClosed (exceptional index) ∧        exceptional index ≠ Set.univ) ∧      (∃ points : OrderedDistinctPoints count, ∀ index, points ∉ exceptional index) ∧      ∀ points : OrderedDistinctPoints count, (∀ index, points ∉ exceptional index) →        ∀ degree : ℕ, 1 ≤ degree →        ∀ polynomial : MvPolynomial (Fin 3) ℂ,

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Atlas selected this possible match because the two statements share words. No review of whether they mean the same thing is recorded.two independent groups report that Comparator accepted runs for this file at the release version shown here.Statement review: none recorded

29 local vocabulary declarationsAllowed axioms: propext, Quot.sound, Classical.choiceopenai/math at fd4aeebwcook04.github.io/plectis-atlas/statements/Nagata.html

Recorded comparisons with the paper

Atlas records no contributed comparison of this statement with the paper.

Contributed Comparator run reports

Atlas records no contributed report of running Comparator for this statement file.

Questions to resolve when comparing this statement with the paper

  • Both independent readers find this family's challenges state less than its headline, while the atlas's AI draft classes this file as stating a paper's theorem as the paper does; check which part of the headline it covers.

Compare this statement with the paperShare a Comparator run reportSuggest a change