{"id":"palomar/PALOMAR-2026-08-26-000013","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/35f4023fda8c9a37287dea03fe9f3487649c919a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-26-000013-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.MG","math.CO","msc:52C10","msc:52C35","msc:51M04","discrete-geometry","combinatorics","lean","formal-verification"],"score":0,"title":"sneed-and-feed/lean-theorems-1","trust":"high","domain":"math.MG","source":"palomar","authors":["Sneed & Feed Formalization Team"],"reviews":0,"subject":"math.MG","summary":"A complete, machine-checked Lean 4 formalization of the Sylvester–Gallai theorem (J. J. Sylvester 1893, T. Gallai 1944, L. M. Kelly 1948; Freek Wiedijk #98). Proves that every finite non-collinear set of points in the real Euclidean plane contains an ordinary line passing through exactly two points of the set, formalized via Kelly's minimal point-line distance argument. To the maintainers' knowledge, the theorem was not found in an exact declaration name, docstring, and type signature search of the pinned Mathlib revision (Mathlib v4.34.0-rc1).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-26","reactions":{},"formalized":true,"formalizes":[{"title":"Mathematical Question 11851","identifier":"","relationship":"formalizes"},{"title":"Solution to Problem 4065","identifier":"","relationship":"formalizes"},{"title":"A problem of collinear points","identifier":"","relationship":"adapts"}]}