Art gallery problem

Stream: Proofs from the book

[Yves Jäckle]

Has the art gallery problem (chapter 39 in edition 5) been formalized (in Lean) ?
Are there any people working on this ?
If not, would anyone be interested in collaborating on it ?
I'm looking for a nice formalization project I can spend around an hour a day on :grinning_face_with_smiling_eyes:

[Snir Broshi]

I think you might need JCT for that, which doesn't exist yet

[Yves Jäckle]

Hmm, it seems we do :sad:
I guess adding necessary facts as assumptions, or just restricting the theorem to the case of triangulable polygons would take the fun out of it too...

[Damiano Testa]

The fact that polygons admit triangulations is much easier than the Jordan curve theorem.

[Yves Jäckle]

It is late in the evening for me and I'll try to talk less nonsense, since I already said
Yves Jäckle said:

triangulable polygons

when what I meant was some thing like "connected regions of the plane that are a finite union of triangles that intersect only at their boundary", and even there I'm not sure I shot myself in the foot :sweat_smile:
I guess Jordan is already needed in the definition ? O'Rourke defines it as:
def.png
(from "Art gallery theorems and algorithms", O'Rourke, 1987)

[Moritz Firsching]

Nice, I have started mathlib bump for the repo:
https://github.com/mo271/FormalBook/pull/88
CI is running, let's see if blueprint also builds...