ProofAtlas

Incidence geometry · formal theorem

Sylvester–Gallai Theorem

A finite set of more than two points in ℝ² that is not all on one line has a pair whose line contains no third point of the set.

Scope: The concrete finite Sylvester-Gallai theorem over ℝ × ℝ: a finite set of more than two points that is not all on one line has an ordinary pair.

Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Sylvester–Gallai incidence mapA finite real-plane set of more than two points that is not all on one line yields a pair whose line contains no third point from the set.
Exact scope: The concrete finite Sylvester-Gallai theorem over ℝ × ℝ: a finite set of more than two points that is not all on one line has an ordinary pair.

Exact formal proposition

Hypotheses and conclusion

This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.

def SylvesterGallaiStatement : Prop :=
  ∀ S : Finset Point, 2 < S.card → ¬ FinsetCollinear S →
    ∃ a b : Point, OrdinaryPair S a b
Definitions used in this proposition

Point

abbrev Point : Type := ℝ × ℝ

Collinear3

def Collinear3 (p q r : Point) : Prop :=
  orientationDet p q r = 0

FinsetCollinear

def FinsetCollinear (S : Finset Point) : Prop :=
  ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ ∀ c ∈ S, Collinear3 a b c

OrdinaryPair

def OrdinaryPair (S : Finset Point) (a b : Point) : Prop :=
  a ∈ S ∧ b ∈ S ∧ a ≠ b ∧
    ∀ c ∈ S, Collinear3 a b c → c = a ∨ c = b
Lean wrapper declaration

The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.

theorem sylvesterGallai :
    SylvesterGallaiStatement
Open main Lean file

Proof route

How score descent forces an ordinary pair

5 proof stages

The checked proof chooses a noncollinear triple of least positive line-point score, normalizes its base, selects adjacent baseline parameters, and shows that any third point on their line would create a strictly smaller score.

These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.

  1. Scientific figure illustrating: Among the finite noncollinear triples, choose one whose squared line distance relative to base length has minimum positive score.
    Among the finite noncollinear triples, choose one whose squared line distance relative to base length has minimum positive score.
    01

    Choose a least positive line-point score

    linePointScore t ≤ linePointScore u

    Finiteness makes the set of noncollinear triples finite, while noncollinearity makes their line-point scores positive. A minimum-score triple supplies the descent invariant: every later candidate must have score at least this chosen value.

    Lean lemmas for this step
    • noncollinearTriples
    • linePointScore
    • linePointScore_pos_of_noncollinear
    • exists_min_linePointScore_noncollinear
  2. Scientific figure illustrating: Translate, rotate, and scale the selected base to a horizontal unit interval while preserving score comparisons.
    Translate, rotate, and scale the selected base to a horizontal unit interval while preserving score comparisons.
    02

    Normalize the selected base to the x-axis

    normalizeToXAxis a b a = (0,0); normalizeToXAxis a b b = (1,0)

    normalizeToXAxis sends the selected endpoints to (0,0) and (1,0), keeps the witness off the axis, and preserves the strict score comparison needed for descent. The remaining argument can therefore use ordered real coordinates on one fixed baseline.

    Lean lemmas for this step
    • normalizeToXAxis
    • normalizeToXAxis_left
    • normalizeToXAxis_right
    • normalizeToXAxis_snd_ne_zero_of_not_collinear3
    • linePointScore_normalizeToXAxis_lt_iff
  3. Two aligned horizontal lines map six collinear set points to six finite real parameters. The blue point a lands exactly on gold 0 and blue b lands exactly on gold 1; one green point lies left of a and another lies right of b.
    The selected endpoints contribute parameters 0 and 1, while the finite baseline set may extend to either side.
    03

    Normalize selected-line points to finite real parameters

    baseLineParameters S a b

    Six discrete points lie on the normalized baseline, with one dashed vertical arrow from each point to a parameter bead at the same horizontal coordinate. The selected cobalt endpoint a aligns with the bead labeled 0, and selected endpoint b aligns with the bead labeled 1. An emerald point and its bead lie strictly left of 0, and another pair lies strictly right of 1, so the pixels do not confine the finite parameter set to the unit interval or suggest a continuum.

    Lean lemmas for this step
    • baseLineParameters
    • mem_baseLineParameters_of_collinear
    • exists_of_mem_baseLineParameters
    • left_mem_baseLineParameters
    • right_mem_baseLineParameters
  4. Scientific figure illustrating: Every location of the witness projection yields a neighboring pair with no baseline parameter strictly between them.
    Every location of the witness projection yields a neighboring pair with no baseline parameter strictly between them.
    04

    Select adjacent parameters around the projection

    choose adjacent x < y around the projection

    The perpendicular projection of the off-line witness lies either between available parameters or beyond one side. The corresponding bracket or one-sided adjacency lemma selects x<y with no recorded baseline parameter between them.

    Lean lemmas for this step
    • exists_projectionLeftAdjacentParameter_of_mem_of_exists_gt
    • exists_projectionRightAdjacentParameter_of_mem_of_exists_lt
    • exists_ordinaryPair_of_min_strict_bracket_baseLineParameters
    • exists_leftAdjacentParametersBeforeProjection_of_forall_lt
    • exists_rightAdjacentParametersAfterProjection_of_forall_gt
    • exists_ordinaryPair_of_min_baseLineParameters
  5. Scientific figure illustrating: A third point on a nonordinary selected line would create a strictly smaller-score triple, so the retained pair is ordinary.
    A third point on a nonordinary selected line would create a strictly smaller-score triple, so the retained pair is ordinary.
    05

    A smaller score contradiction leaves an ordinary pair

    ¬ OrdinaryPair(a,b) → ∃ w ∈ noncollinearTriples(S), linePointScore(w) < linePointScore(a,b,p)

    If the adjacent pair were not ordinary, another set point would lie on its line. The normalization and adjacency inequalities then construct a noncollinear triple with score below the chosen minimum, a contradiction; hence exactly the selected two set points lie on the line.

    Lean lemmas for this step
    • exists_collinear_ne_of_not_ordinaryPair
    • exists_descent_of_adjacent_baseLineParameters
    • ordinary_or_descent_of_adjacent_baseLineParameters
    • exists_ordinaryPair_of_min_adjacent_baseLineParameters
    • exists_ordinaryPair_of_min_baseLineParameters
    • sylvesterGallai

The theorem at a glance

Sylvester–Gallai at a glance

Editorial incidence-geometry poster with a finite non-collinear point constellation and one gold ordinary line through exactly two ringed set points, plus the minimum-score proof architecture and finite real-plane scope boundary.
Every finite non-collinear subset of the real affine plane with more than two points determines a line containing exactly two set points.

Accessible transcript

2 < S.card ∧ ¬FinsetCollinear S ⇒ ∃ a b, OrdinaryPair S a b

The checked proof chooses a noncollinear triple of minimum positive line-point score, normalizes its base, and selects adjacent parameters on that line. Any third set point on the selected line would create a triple with smaller score, so the remaining pair is ordinary. The argument is finite and specific to the real affine plane.

Read the complete poster transcript

INCIDENCE GEOMETRY · REAL AFFINE PLANE

SYLVESTER–GALLAI THEOREM

ONE LINE · EXACTLY TWO SET POINTS

FOR EVERY FINITE S ⊂ ℝ²

|S| > 2 · S IS NOT COLLINEAR

S DETERMINES AN ORDINARY LINE

An ordinary line contains exactly two points of S.

HOW THE PROOF MOVES

1 · CHOOSE A MINIMUM TRIPLE

Minimize a positive line-to-point score.

2 · NORMALIZE THE BASE LINE

Send its endpoints to (0,0) and (1,0).

3 · ISOLATE AN ADJACENT GAP

If a third set point lies on the base line, use neighboring parameters.

4 · FORCE A SMALLER SCORE

The new triple contradicts minimality; an ordinary pair remains.

EXACT SCOPE

Finite subsets of the concrete real affine plane. Not an infinite, projective, or abstract incidence-space theorem.

Theorem schematic

One ordinary line in a finite constellation

Scientific figure illustrating: Every finite non-collinear real planar set with more than two points determines an ordinary line containing exactly two set points.
Every finite non-collinear real planar set with more than two points determines an ordinary line containing exactly two set points.

finite S ⊂ ℝ² ∧ |S| > 2 ∧ ¬collinear(S) ⇒ ∃ ordinary pair in S

Among any finite noncollinear real planar set with more than two points, there are two set points whose line contains no third point of the set. That pair is the ordinary-pair witness asserted by the theorem.

Result boundary

What this theorem does—and does not—establish

The concrete finite Sylvester-Gallai theorem over ℝ × ℝ: a finite set of more than two points that is not all on one line has an ordinary pair.

About these visual explanations

These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

Continue the mathematics

Open questions and extensions

The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.

What the source ZIP contains

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.

Complete checked Lean source · 1 Lean file · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Publication review

Review record

Publication reviews accepted

Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.

01

Formal evidence

The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.

02

Statement alignment

The formal declaration was accepted against the named theorem and its exact variant.

03

Result boundary

The accepted boundary keeps nearby stronger or commonly confused claims out of scope.

04

Public wording

The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.

05

Canonical source

The first-party source link is pinned to the checked package commit and exact Lean file.

06

Accepted result

A validated accepted-result record binds the four reviews to the checked formalization.

Expanded visual

Open original image