Sebastien Gouezel (Sep 30 2020 at 20:49):
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.
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!
Last updated: May 11 2021 at 16:22 UTC