Erdős Problem #189
DISPROVED LEANdatabase updated 2025-12-19
The statement as posed is false. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Erdős problem 189 asked whether the below holds for all rectangles.
If \(\mathbb{R}^2\) is finitely coloured then must there exist some colour class which contains the vertices of a rectangle of every area? Graham, "On Partitions of 𝔼ⁿ", Journal of Combinatorial Theory, Series A 28, 89-91 (1980). (See "Concluding Remarks" on page 96.) Solved (with answer `False`, as formalised below) in: Vjekoslav Kovač, "Coloring and density theorems for configurations of a given volume", 2023 https://arxiv.org/abs/2309.09973 In fact, Kovač's colouring is even Jordan measurable (the topological boundary of each monochromatic region is Lebesgue measurable and has measure zero). This was formalized in Lean by Alexeev and Kovac using Aristotle.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/189.Prizenone
Topicsgeometry, ramsey theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/189
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.