Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 224

claims/: The 1 claim page of Problem 224, one per claimant's result; the problem's standing derives from them.

Statement. If $A\subseteq \mathbb{R}^d$ is any set of $2^d+1$ points then some three points in $A$ determine an obtuse angle.

Statement (precise). If $A\subseteq \mathbb{R}^d$ is any set of $2^d+1$ points then some three points in $A$ determine an obtuse angle, that is, an angle greater than a right angle, a straight angle included.

Notes. "Obtuse" is read as an angle greater than a right angle, a straight angle included, as Erdős's formulation (every angle at most a right angle) and Danzer and Grünbaum's theorem read it. Read strictly, the site's wording fails at $d=1$ (three collinear points) and at $d=2$ (a square and its center). The formal-conjectures statement and the linked Lean file use the inclusive reading, as the claim page explains.

Status. PROVED (LEAN): the site labels the problem proved with a Lean qualification. The theorem is Danzer and Grünbaum's, recorded on the Danzer–Grünbaum claim page; the Lean proof the label refers to is a third-party development, linked from that page and under Formalization, which this corpus has not built.

Source. erdosproblems.com/224, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #224, https://www.erdosproblems.com/224.

References.

[DaGr62] Danzer, L. and Grünbaum, B., Über zwei Probleme bezüglich konvexer Körper von P. Erdős und von V. L. Klee. Math. Z. (1962), 95-99.

Formalization. Statement in formal-conjectures, which at that commit marks the problem solved with a sorry in place of the proof and points to a Lean 4 proof in plby/lean-proofs that declares itself a formalization of Danzer and Grünbaum's solution, with GPT-5.2 Thinking, Codex and Coder-Osman, the person who posted it, named as its formal authors; this corpus has not built or audited either file, so the formalization is a link, not acceptance evidence.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (7)

problems/discrete_geometry/E0224/claims Discrete and Convex Geometry discrete_geometry/danzer_1962_zwei_probleme_konvexer_korper_erdos_klee Satz I (p. 96): no obtuse triangle implies antipodal, antipodal sets as touching translates, and Minkowski symmetrization Satz II (p. 96): e_n = k_n = l_n = m_n = m_n* = 2^n, with parallelotopes extremal discrete_geometry/erdos_1960_extremum_problems_elementary_geometry Conjecture, p. 54: among 2^n + 1 points in n-space some angle exceeds pi/2, proved by Danzer and Grünbaum per a note added in proof

Graph