complex_lines_problem
Provedgeometry
Sylvester-Gallai in ℂ (Kelly's theorem 1986): If every line through 2 points in ℂⁿ contains a 3rd, all points are collinear. Generalizations to higher fields and varieties remain open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem complex_lines_problem (n : ℕ) (hn : 3 ≤ n)
(pts : Fin n → ℂ)
(hinj : Function.Injective pts)
(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
sorrySource