{"id":"palomar/PALOMAR-2026-08-29-000013","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/f72d0d60a7ba8c8a4789e03bb6be0f9d007bea64","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000013-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","math.MG","msc:52C10","msc:05D10","msc:52A10","combinatorial-geometry","lean-formalization","erdos-szekeres","convex-polygons"],"score":0,"title":"sneed-and-feed/lean-theorems-1","trust":"high","domain":"math.CO","source":"palomar","authors":["Sneed & Feed Formalization Team"],"reviews":0,"subject":"math.CO","summary":"A comprehensive, machine-checked Lean 4 formalization of the Erdős–Szekeres Convex Polygon Theorem (1935). Formalizes orientation determinants, general position, 2D rotation transformations with finite slope avoidance (rotating any finite set to have mutually distinct x-coordinates), x-coordinate sorting, cup-cap sequences with Pascal-type binomial split recurrences, halfspace separation for convex hulls, and rotation invariance of convex polygons. Proves that any finite set of at least choose(2k - 4, k - 2) + 1 points in general position in ℝ² contains the vertices of a strictly convex…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-29","reactions":{},"formalized":true,"formalizes":[{"title":"A combinatorial problem in geometry","identifier":"","relationship":"formalizes"}]}