Open Research Index

The Art Gallery Problem is ∃ℝ-complete: point-point, boundary-point and point-boundary variants, in Lean 4

Robert D. Barish

Palomar Registrypalomar/PALOMAR-2026-10-27-000025Oct 27, 2026cs.CGscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-27-000025
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-27-000025/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-27-000025/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'