Status
On this page
Status
Topics
Status
On this page
Status
Topics
If is any set of points then some three points in determine an obtuse angle.
If is any set of points then some three points in determine an obtuse angle, that is, an angle greater than a right angle, a straight angle included.
Source: erdosproblems.com/224
An accepted solution exists. The statement is true.
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 (1962); 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.
"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 (three collinear points) and at (a square and its center). The formal-conjectures statement and the linked Lean file use the inclusive reading, as the claim page explains.