Happy Ending Problem #
The happy ending problem asks whether $f(n) = 2^{n-2} + 1$, where $f(n)$ is the smallest number such that any $f(n)$ points in general position in the plane contain $n$ that form a convex polygon.
Reference: Wikipedia
This file points to the canonical formalization in FormalConjectures.ErdosProblems.«107».