{"id":"palomar/PALOMAR-2026-10-27-000025","url":"https://github.com/RBarish-UTokyo/ArtGalleryProblem-ExistsR-Lean4/tree/7bfe29cbdad3b057fc5e83397973d554773282e6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000025-v1.json","repo":"https://github.com/RBarish-UTokyo/ArtGalleryProblem-ExistsR-Lean4","tags":["cs.CG","cs.CC","msc:68U05","msc:68Q17","msc:14P10","msc:68V20"],"score":0,"title":"The Art Gallery Problem is ∃ℝ-complete: point-point, boundary-point and point-boundary variants, in Lean 4","trust":"high","domain":"cs.CG","source":"palomar","authors":["Robert D. Barish"],"reviews":0,"subject":"cs.CG","summary":"A Lean 4 and Mathlib formalization of Abrahamsen, Adamaszek and Miltzow, \"The Art Gallery Problem is ∃ℝ-complete\" (J. ACM 2021), together with Stade's point-boundary variant (SoCG 2025), for an explicit single-tape Turing machine model. Lean proves that deciding whether a simple polygon with rational corners can be guarded by g guards is ∃ℝ-complete under polynomial-time many-one reductions in each of the three variants known to be ∃ℝ-complete: point guards guarding the whole polygon (Theorem 1, also for integer corners), guards on the boundary guarding the whole polygon (the boundary-point…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"The Art Gallery Problem is ∃ℝ-complete","identifier":"","relationship":"formalizes"},{"title":"The Point-Boundary Art Gallery Problem is ∃ℝ-hard","identifier":"arXiv:2210.12817v3","relationship":"formalizes"}]}