The orthogonal art gallery problem is ∃ℝ-complete (point-point and point-boundary), in Lean 4
A Lean 4 formalization of material in a forthcoming manuscript entitled "The Orthogonal Art Gallery Problem is ∃ℝ-complete". A Lean 4 and Mathlib proof, for an explicit single-tape Turing machine model, that deciding whether an orthogonal simple polygon (every edge horizontal or vertical) with rational corners can be guarded by g guards is ∃ℝ-complete under polynomial-time many-one reductions, both when the guards must see the whole polygon (point-point) and when they must see only its boundary (point-boundary). Both problems also reduce to ETR by formulas whose only variables are the 2g…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000004/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-11-01-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'