Lean repository linked
The Point-Boundary Art Gallery Problem is ∃ℝ-hard
arXiv:2210.12817 · arXiv
Lean formalisations (1)
RBarish-UTokyo/ArtGalleryProblem-ExistsR-Lean4 at 7bfe29cbdad3
Linked by the repository’s formalization.yaml.
Project review: agent-reviewed
Audit: awaiting publication.