Formal target: Corpus.Arxiv11024662AtiyahSutcliffe.conjecture_one

Atiyah–Sutcliffe Conjecture 1, stated as Conjecture 1.1 in Mazur–Petrenko: the configuration polynomials are linearly independent.

Exact formal statement

∀ {n : Nat} (x : Fin n → Corpus.Arxiv11024662AtiyahSutcliffe.Point),
  Function.Injective.{1, 1} x →
    LinearIndependent.{0, 0, 0} Complex (Corpus.Arxiv11024662AtiyahSutcliffe.pointPolynomial x)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record