{"id":"palomar/PALOMAR-2026-10-05-000003","url":"https://github.com/RBarish-UTokyo/LinearTimeTriangulation-ChazelleAlgorithm-Lean4/tree/92cc7745aa026aad3e80e7a72fe88cfbd909614a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-05-000003-v2.json","repo":"https://github.com/RBarish-UTokyo/LinearTimeTriangulation-ChazelleAlgorithm-Lean4","tags":["cs.CG","msc:68U05","msc:68Q25","msc:68W40","msc:52B55","computational-geometry","polygon-triangulation","algorithms","lean-formalization"],"score":0,"title":"Linear-Time Triangulation of Simple Polygons (Chazelle's Algorithm) in Lean 4","trust":"high","domain":"cs.CG","source":"palomar","authors":["Robert D. Barish"],"reviews":0,"subject":"cs.CG","summary":"A formalization and provably correct implementation of a linear-time algorithm for triangulating a simple polygon. The implementation is a concrete program for an explicit exact real RAM. Lean proves that on every simple polygon with n vertices the program halts within C(n+1) steps, with natural-number words at most K(n+1), and outputs a conforming triangulation with exactly n - 2 triangles on the input vertices. No general-position assumption is made. The proofs use exactly Lean's three standard axioms (propext, Classical.choice, Quot.sound), with no sorry and no native_decide. They are…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-05","reactions":{},"formalized":true,"formalizes":[{"title":"Triangulating a simple polygon in linear time","identifier":"doi:10.1007/BF02574703","relationship":"formalizes"}]}