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

Updated Oct 8

Problem 214

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

Statement. Let $S\subset \mathbb{R}^2$ be such that no two points in $S$ are distance $1$ apart. Must the complement of $S$ contain four points which form a unit square?

Status. Proved. Juhász's 1979 theorem gives the stronger conclusion that the complement contains a congruent copy of every prescribed four-point set. The site's label, PROVED (LEAN), carries a Lean qualifier that refers to the public formalizations discussed below; this corpus has built neither of them. The theorem is recorded in claims/ as an accepted claim, from which the problem's standing derives.

Source. T. F. Bloom, Erdős Problem #214, with its discussion and proof-claim thread. The page was last edited April 2, 2026. The site's original locator is [Er83c, p. 47], Erdős's 1983 survey Combinatorial problems in geometry, carded as erdos_1983_combinatorial_problems_geometry. The solved square question is separate from the still-undetermined general configuration threshold treated below.

References.

R. Juhász, Ramsey type theorems in the plane, Journal of Combinatorial Theory, Series A 27 (1979), 152–160, doi:10.1016/0097-3165(79)90042-6.
G. Csizmadia and G. Tóth, Note on a Ramsey-Type Problem in Geometry, Journal of Combinatorial Theory, Series A 65 (1994), 302–306, doi:10.1016/0097-3165(94)90025-6.
P. Erdős, R. L. Graham, P. Montgomery, B. L. Rothschild, J. Spencer and E. G. Straus, Euclidean Ramsey Theorems, II, Infinite and Finite Sets, Colloquia Mathematica Societatis János Bolyai 10 (1975), 529–557.
D. Conlon and J. Fox, Lines in Euclidean Ramsey Theory, Discrete & Computational Geometry 61 (2019), 218–225, doi:10.1007/s00454-018-9980-5.

Formalization. The Current assessment below records the public formalizations; this corpus has built none of them.

Current assessment

The threshold $\kappa$ is defined in the later section "The related universal configuration threshold".

The site reports $4\le\kappa\le7$ as the best-known bounds. Neither the original geometric papers nor the later primary literature carded in the library, such as the Conlon–Fox paper, records a five-point or eight-point result improving this general planar interval. Later results about higher dimensions or particular collinear configurations do not change the exact square question or automatically improve $\kappa$ .

Wouter van Doorn's March 2, 2026 announcement attributes formalizations of both Juhász theorems to the AI system Aristotle from Harmonic. The pinned four-point file and twelve-point file declare those respective targets over the Euclidean plane and identify Lean 4.24.0 and the mathlib commit their headers record.

The pinned formal-conjectures statement contains sorry in its main theorem and five variants. Its proof metadata points to the separate formalization in Alexeev's lean-proofs repository, which declares both Juhász results for Lean and mathlib 4.29.1. This corpus has not built or audited either development, so neither is evidence of acceptance. The ordinary mathematical proof and these public formalization records are distinct evidence.

The accepted claim page [[problems/distance_problems/E0214/claims/1979_09_01_juhasz|records Juhász's four-point theorem]] with its refereed publication, the curator's credit and the two public formalizations linked at pinned commits; the problem's standing derives from it.

The complete ordinary proof

Color $S$ blue and its complement red. This gives exactly the hypothesis of Juhász's Theorem 1. Apply it to $K=\{(0,0),(1,0),(1,1),(0,1)\}$ . The resulting red congruent copy lies in the complement of $S$ and is the required unit square.

The complete source proof treats three cases: a parallelogram whose side lengths are forbidden blue distances, a configuration all of whose distances are forbidden in blue, and a realized blue distance whose opposite pair has a different midpoint. Red rhombi, successive rotations, complementary circles and growing radii supply the respective arguments. The source's lemmas and exact geometric cases are compiled separately, including the small-separation circle intersection. No measurability or other regularity of the coloring is assumed.

The earlier three-dimensional square theorem is not by itself this planar proof.

Let $\kappa$ be the largest integer $n$ such that every planar coloring with no blue unit-distance pair contains a red congruent copy of every $n$ -point configuration. The compiled primary results give

4\le\kappa\le7.

The lower bound is Juhász's four-point theorem. Juhász's twelve-point construction gives the historical upper bound eleven. Csizmadia–Tóth's eight-point construction improves it to seven, using a radius- $9/10$ regular heptagon together with its center. Exchanging the color names matches that paper's convention.

The forcing property is downward closed: extend any smaller finite set to an $n$ -point set and restrict the resulting congruent copy. Conversely, extending an eight-point counterconfiguration shows failure for every larger size. Thus these bounds concern a well-defined finite maximum. They do not assert that every seven-point set is forced.

Csizmadia–Tóth's five-point proposition applies only to their specific lattice-disk coloring and to translates. It does not establish $\kappa\ge5$ for arbitrary colorings. Likewise, the five-point collinear conclusion relevant to Problem 188 does not force every possible five-point shape.

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 (58)

Graph