torsion_anomalous_conjecture

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Bombieri-Masser-Zannier torsion anomalous conjecture: A variety V in a multiplicative algebraic torus has only finitely many torsion anomalous points (points lying in a torsion coset of dimension > n - dim V). Proved for curves (Bays-Habegger 2015); higher dimensions open.

Why this node was retired

The posted statement is

import Mathlib

theorem torsion_anomalous_conjecture (n : ℕ) (hn : 2 ≤ n)
    (V : Set (Fin n → ℂ))
    (hV : ∃ (polys : List (MvPolynomial (Fin n) ℂ)),
      V = {x | ∀ p ∈ polys, MvPolynomial.eval x p = 0}) :
    {x ∈ V | ∃ m : ℕ, 1 ≤ m ∧ ∀ i : Fin n, (x i) ^ m = 1}.Finite := by
  sorry

The target counts all torsion points on any affine algebraic set, omitting the anomalous-intersection geometry and exceptional-locus qualifications.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

No single faithful repair follows from the abbreviated prose. Specify an irreducible subvariety V⊂(G_m)^n, torsion cosets, the precise anomalous dimension inequality and maximality/exceptional-locus conventions, then formulate the intended finiteness assertion for the resulting exceptional subvarieties or points. The simple claim that all torsion points of arbitrary V are finite must be removed.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.