Erdős Problem #107
'Happy Ending' problem
FALSIFIABLEdatabase updated 2025-08-31
Still open — but if it is false, a finite counterexample exists, so a computer search could in principle disprove it. A search can't prove it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The set of \(N\) such that any \(N\) points in the plane, no three on a line, contain a convex \(n\)-gon.
The function \(f(n)\) specified in `erdos_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\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/107.Prize$500
Statement in LeanFormal Conjectures
Solution in Leanno
OEISA000051
Original pageerdosproblems.com/107
Attempts
submit one →Read our working report →
Explicitly verified a 32-point integer \(n=7\) lower-bound witness, certified the sharp \((7,4,7)\) constrained regime in a stronger signotope relaxation with two SAT engines, and reduced the open 33-
PARTIAL