Pascal's theorem

pascal

Submitter: Kim Morrison.

Notes: Six distinct points on a non-singular conic determine three collinear intersection points Aᵢ Bⱼ ∩ Aⱼ Bᵢ. Trusted helpers (SamePoint, OnConic, meet, Collinear3) are non-holes, built on the cross product ⨯₃. Mathlib has the projective vocabulary but not Pascal's theorem. Candidate from §146 of the Knill survey.

Source: B. Pascal, *Essay pour les coniques* (1640). Knill, *Some fundamental theorems in mathematics*, §146.

Informal solution: Project-and-compute, or the classical synthetic proof. Algebraically: choose homogeneous coordinates; the conic is xᵀMx=0. The three meet points' collinearity is a polynomial identity in the six points' coordinates that holds on the conic — provable by a Gröbner/resultant computation, or synthetically via the converse of Menelaus applied to the hexagon, or as the d=2 Cayley–Bacharach instance (a cubic through 8 of the 9 base points of two degenerate cubics passes through the 9th). None of this packaging is in Mathlib.

theorem declaration uses `sorry`pascal (M : Matrix (Fin 3) (Fin 3) ℝ) (hMsymm : M.IsSymm) (hMdet : M.det ≠ 0)
    (a₁ a₂ a₃ b₁ b₂ b₃ : Fin 3 → ℝ)
    (ha₁ : a₁ ≠ 0) (ha₂ : a₂ ≠ 0) (ha₃ : a₃ ≠ 0)
    (hb₁ : b₁ ≠ 0) (hb₂ : b₂ ≠ 0) (hb₃ : b₃ ≠ 0)
    (hdist : [a₁, a₂, a₃, b₁, b₂, b₃].Pairwise (fun v w => ¬ LeanEval.Geometry.PascalPappus.SamePoint v w))
    (hA₁ : LeanEval.Geometry.PascalPappus.OnConic M a₁) (hA₂ : LeanEval.Geometry.PascalPappus.OnConic M a₂) (hA₃ : LeanEval.Geometry.PascalPappus.OnConic M a₃)
    (hB₁ : LeanEval.Geometry.PascalPappus.OnConic M b₁) (hB₂ : LeanEval.Geometry.PascalPappus.OnConic M b₂) (hB₃ : LeanEval.Geometry.PascalPappus.OnConic M b₃) :
    LeanEval.Geometry.PascalPappus.Collinear3 (LeanEval.Geometry.PascalPappus.meet a₁ b₂ a₂ b₁) (LeanEval.Geometry.PascalPappus.meet a₁ b₃ a₃ b₁) (LeanEval.Geometry.PascalPappus.meet a₂ b₃ a₃ b₂) := byM:Matrix (Fin 3) (Fin 3) ℝhMsymm:M.IsSymmhMdet:M.det ≠ 0a₁:Fin 3 → ℝa₂:Fin 3 → ℝa₃:Fin 3 → ℝb₁:Fin 3 → ℝb₂:Fin 3 → ℝb₃:Fin 3 → ℝha₁:a₁ ≠ 0ha₂:a₂ ≠ 0ha₃:a₃ ≠ 0hb₁:b₁ ≠ 0hb₂:b₂ ≠ 0hb₃:b₃ ≠ 0hdist:List.Pairwise (fun v w => ¬SamePoint v w) [a₁, a₂, a₃, b₁, b₂, b₃]hA₁:OnConic M a₁hA₂:OnConic M a₂hA₃:OnConic M a₃hB₁:OnConic M b₁hB₂:OnConic M b₂hB₃:OnConic M b₃⊢ Collinear3 (meet a₁ b₂ a₂ b₁) (meet a₁ b₃ a₃ b₁) (meet a₂ b₃ a₃ b₂)
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 10, 2026