From eb557e366aa53f7fa581c8d5c81c5793dcc3efd9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 9 Jun 2026 07:46:06 +0000 Subject: [PATCH 1/3] =?UTF-8?q?feat:=20add=20Pascal=20and=20Pappus=20theor?= =?UTF-8?q?ems=20eval=20problems=20(=C2=A7146)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 4.8 (1M context) --- LeanEval/Geometry/PascalPappus.lean | 58 +++++++++++++++++++++++++++++ manifests/problems/pappus.toml | 9 +++++ manifests/problems/pascal.toml | 9 +++++ 3 files changed, 76 insertions(+) create mode 100644 LeanEval/Geometry/PascalPappus.lean create mode 100644 manifests/problems/pappus.toml create mode 100644 manifests/problems/pascal.toml diff --git a/LeanEval/Geometry/PascalPappus.lean b/LeanEval/Geometry/PascalPappus.lean new file mode 100644 index 0000000..33c1cd7 --- /dev/null +++ b/LeanEval/Geometry/PascalPappus.lean @@ -0,0 +1,58 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval.Geometry.PascalPappus + +/-! +# Pascal's theorem and Pappus's hexagon theorem + +`pascal` (Pascal 1639): six points on a non-singular conic give three collinear +intersection points. `pappus` (Pappus, c. 320 AD): the degenerate-conic case +with the six points on two lines. Trusted helpers (`SamePoint`, `OnConic`, +`meet`, `Collinear3`) are non-holes. Mathlib has the cross product `⨯₃` and +projective vocabulary but neither theorem. +Category-(b) candidates from §146 of the Knill survey. +-/ + +open Matrix + +/-- Two homogeneous coordinate vectors represent the same projective point. -/ +def SamePoint (v w : Fin 3 → ℝ) : Prop := ∃ c : ℝ, c ≠ 0 ∧ w = c • v + +/-- `[v]` lies on the conic `xᵀ M x = 0`. -/ +def OnConic (M : Matrix (Fin 3) (Fin 3) ℝ) (v : Fin 3 → ℝ) : Prop := + v ⬝ᵥ (M *ᵥ v) = 0 + +/-- Intersection (meet) of line `[a][b]` and line `[c][d]`. -/ +def meet (a b c d : Fin 3 → ℝ) : Fin 3 → ℝ := (a ⨯₃ b) ⨯₃ (c ⨯₃ d) + +/-- Three projective points are collinear (vanishing triple product). -/ +def Collinear3 (p q r : Fin 3 → ℝ) : Prop := p ⬝ᵥ (q ⨯₃ r) = 0 + +/-- **Pascal's theorem.** Six distinct points on a non-singular conic determine +three collinear intersection points `Aᵢ Bⱼ ∩ Aⱼ Bᵢ`. -/ +@[eval_problem] +theorem 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 => ¬ SamePoint v w)) + (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₂) := by + sorry + +/-- **Pappus's hexagon theorem.** With `A₁,A₂,A₃` collinear and `B₁,B₂,B₃` +collinear, the three intersection points `Aᵢ Bⱼ ∩ Aⱼ Bᵢ` are collinear. -/ +@[eval_problem] +theorem pappus + (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 => ¬ SamePoint v w)) + (hA : Collinear3 a₁ a₂ a₃) (hB : Collinear3 b₁ b₂ b₃) : + Collinear3 (meet a₁ b₂ a₂ b₁) (meet a₁ b₃ a₃ b₁) (meet a₂ b₃ a₃ b₂) := by + sorry + +end LeanEval.Geometry.PascalPappus diff --git a/manifests/problems/pappus.toml b/manifests/problems/pappus.toml new file mode 100644 index 0000000..d805ead --- /dev/null +++ b/manifests/problems/pappus.toml @@ -0,0 +1,9 @@ +id = "pappus" +title = "Pappus's hexagon theorem" +test = false +module = "LeanEval.Geometry.PascalPappus" +holes = ["pappus"] +submitter = "Kim Morrison" +notes = "With A₁,A₂,A₃ collinear and B₁,B₂,B₃ collinear, the three intersection points Aᵢ Bⱼ ∩ Aⱼ Bᵢ are collinear — the degenerate-conic limit of Pascal. Shares the §146 trusted helpers (SamePoint, OnConic, meet, Collinear3). Not in Mathlib. Candidate from §146 (additional 1)." +source = "Pappus of Alexandria, *Collection*, Book VII (c. 320 AD). Knill, *Some fundamental theorems in mathematics*, §146." +informal_solution = "The degenerate case of Pascal with the conic = a pair of lines (the two triples of collinear points). Algebraically the collinearity of the three meet points is a multilinear identity in the six points' homogeneous coordinates given the two collinearity constraints; provable by direct cross-product computation (meet = (a×b)×(c×d), collinearity = triple product zero) and elimination, or as the projective incidence theorem underlying the commutativity of the coordinate field (Hilbert). Not in Mathlib." diff --git a/manifests/problems/pascal.toml b/manifests/problems/pascal.toml new file mode 100644 index 0000000..5bc45ad --- /dev/null +++ b/manifests/problems/pascal.toml @@ -0,0 +1,9 @@ +id = "pascal" +title = "Pascal's theorem" +test = false +module = "LeanEval.Geometry.PascalPappus" +holes = ["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." From 16f209a40983b98faa4c3af23584d879e8f343ca Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 9 Jun 2026 07:50:29 +0000 Subject: [PATCH 2/3] fix: drop Pappus (junk-true vacuity: six collinear points collapse the meet points); keep Pascal --- manifests/problems/pappus.toml | 9 --------- 1 file changed, 9 deletions(-) delete mode 100644 manifests/problems/pappus.toml diff --git a/manifests/problems/pappus.toml b/manifests/problems/pappus.toml deleted file mode 100644 index d805ead..0000000 --- a/manifests/problems/pappus.toml +++ /dev/null @@ -1,9 +0,0 @@ -id = "pappus" -title = "Pappus's hexagon theorem" -test = false -module = "LeanEval.Geometry.PascalPappus" -holes = ["pappus"] -submitter = "Kim Morrison" -notes = "With A₁,A₂,A₃ collinear and B₁,B₂,B₃ collinear, the three intersection points Aᵢ Bⱼ ∩ Aⱼ Bᵢ are collinear — the degenerate-conic limit of Pascal. Shares the §146 trusted helpers (SamePoint, OnConic, meet, Collinear3). Not in Mathlib. Candidate from §146 (additional 1)." -source = "Pappus of Alexandria, *Collection*, Book VII (c. 320 AD). Knill, *Some fundamental theorems in mathematics*, §146." -informal_solution = "The degenerate case of Pascal with the conic = a pair of lines (the two triples of collinear points). Algebraically the collinearity of the three meet points is a multilinear identity in the six points' homogeneous coordinates given the two collinearity constraints; provable by direct cross-product computation (meet = (a×b)×(c×d), collinearity = triple product zero) and elimination, or as the projective incidence theorem underlying the commutativity of the coordinate field (Hilbert). Not in Mathlib." From 68a8eaeeb80525d319c612e5edf8aad584cf5de3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 9 Jun 2026 07:50:59 +0000 Subject: [PATCH 3/3] fix: actually remove the Pappus theorem body from the module (manifest already dropped) --- LeanEval/Geometry/PascalPappus.lean | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/LeanEval/Geometry/PascalPappus.lean b/LeanEval/Geometry/PascalPappus.lean index 33c1cd7..c341780 100644 --- a/LeanEval/Geometry/PascalPappus.lean +++ b/LeanEval/Geometry/PascalPappus.lean @@ -43,16 +43,4 @@ theorem pascal Collinear3 (meet a₁ b₂ a₂ b₁) (meet a₁ b₃ a₃ b₁) (meet a₂ b₃ a₃ b₂) := by sorry -/-- **Pappus's hexagon theorem.** With `A₁,A₂,A₃` collinear and `B₁,B₂,B₃` -collinear, the three intersection points `Aᵢ Bⱼ ∩ Aⱼ Bᵢ` are collinear. -/ -@[eval_problem] -theorem pappus - (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 => ¬ SamePoint v w)) - (hA : Collinear3 a₁ a₂ a₃) (hB : Collinear3 b₁ b₂ b₃) : - Collinear3 (meet a₁ b₂ a₂ b₁) (meet a₁ b₃ a₃ b₁) (meet a₂ b₃ a₃ b₂) := by - sorry - end LeanEval.Geometry.PascalPappus