sylvester_gallai_complex

⚠️ Retired — specification defect

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

Sylvester-Gallai over ℂ (Kelly's theorem): Any finite set of points in ℂ^n where every line through 2 points contains a 3rd point is collinear (actually a theorem of Kelly 1986). Extensions and analogs in higher dimensions remain open.

Why this node was retired

The posted statement is

import Mathlib

theorem sylvester_gallai_complex (n : ℕ) (hn : 3 ≤ n)
    (pts : Fin n → ℂ)
    (hcoll : ∀ a b c : Fin n, a ≠ b → b ≠ c → a ≠ c →
      ∃ t : ℂ, pts a = pts b + t * (pts c - pts b)) :
    ∃ a b c : Fin n, a ≠ b ∧ b ≠ c ∧ a ≠ c ∧
      ∀ d : Fin n, ∃ t : ℂ, pts d = pts a + t * (pts b - pts a) := by
  sorry

The hypothesis already says every triple of distinct indexed points is collinear, replacing the intended ordinary-line hypothesis.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

For a finite noncollinear set S⊂ℂᵈ such that every line through two points of S contains a third point of S, conclude that the affine complex span of S has dimension at most 2 (the complex Sylvester–Gallai/Kelly statement). If the intended target is a different complex variant, specify it before formalizing.

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.