Reasonable theorem to formalize

Stream: maths

[Sebastien Gouezel]

I just came across a beautiful theorem, that seems to be a good target for formalization: nontrivial, important (published in JAMS in 2017, on a problem of Erdos dating back to 1935), short (6 pages), without too much background (planar geometry and convex sets) but raising nontrivial formalization issues (planar geometry and convex sets). I won't have time any time soon to work on this, but since the theorem is fun I thought I would mention it here.

Let n be an integer. Consider 4^n points in the plane. Then you can find n of them which are in convex position (i.e., they are all on the boundary of their convex hull). This was proved by Erdös and Szekeres in 1935. But 4^n is definitely not optimal. How better can you do? A lower bound 2^n was found by Erdös in 1960, but there is huge gap between these bounds. Suk (J. Amer. Math. Soc. 30 (2017), 1047-1053) shows that 2^(n + o(n)) points are enough.

You can try proving the theorem even without any nice bound, it's really fun!