Erdős problem 107

Let $f(n)$ be minimal such that any $f(n)$ points in $ℝ^2$ , no three on a line, contain $n$ points which form the vertices of a convex $n$ -gon. Prove that $f(n) = 2^{n-2} + 1$ .

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

107.lean

Retained formal statement4 of 7

For every $n ≥ 3$ , there exists $N$ such that any $N$ points, no three on a line, contain a convex $n$ -gon.

FormalConjectures/ErdosProblems/107.leanErdos107.nonempty_cardSet1 lineExact file

1∀ n ≥ 3, (Erdos107.cardSet n).Nonempty

SolvedStatement only, no proof