FormalConjectures/Wikipedia/HappyEndingProblem.lean
0 declarations, 0 contain sorry, 0 declared as axioms
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».
No declarations listed.