Erdős Problem #504
Blumenthal's problem
SOLVEDdatabase updated 2025-08-31
Resolved in some way other than a straight proof or disproof — usual for open-ended questions, or for multi-part problems whose parts went different ways.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The minimax angle \(\alpha_N\): the supremum of all \(\alpha \in [0, \pi]\) such that every set of \(N\) points of the plane contains three pairwise distinct points \(x, z, y\) with \(\angle x z y \ge \alpha\) (angle taken at the middle point \(z\)).
**Erdős–Szekeres (1960).** For \(n \ge 3\), \(\alpha_{2^n} = \pi\left(1 - \frac{1}{n}\right)\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 5 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/504.Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/504
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.