---

Claim. Let the plane be colored red and blue so that no two blue points are at distance one. Then for every set $K\subset\mathbb R^2$ of four distinct points there is a red congruent copy of $K$: a set obtained from $K$ by a rotation, a translation and possibly a reflection, all of whose points are red. Applied to the coloring that paints a set $S$ avoiding distance one blue and its complement red, with $K$ the four vertices of a unit square, this answers the question of Problem 214 affirmatively: the complement of $S$ contains four points forming a unit square. No measurability or other regularity of $S$ is assumed, and the copy may have any position and orientation.

The argument. The proof is Theorem 1 of the paper and splits into three cases according to which distances of $K$ occur between blue points: a parallelogram neither of whose side lengths is a blue distance, a set none of whose six distances is a blue distance, and a pair of points of $K$ at a blue distance whose segment has a different midpoint from the segment joining the other two points. Red rhombi, rotations about a vertex, pairs of complementary circles and a sequence of growing radii supply the three arguments. The library's [[../library/distance_problems/juhasz_1979_ramsey_type_theorems_plane/theorem_1|reconstruction of Theorem 1]] gives the complete proof with its four lemmas and the radius estimates, from the published paper, and the [[../library/distance_problems/juhasz_1979_ramsey_type_theorems_plane/_index|source card]] records the conventions and the complete chain. The paper's second theorem, a twelve-point set that some unit-distance-avoiding coloring keeps out of red, bounds the general configuration threshold discussed on the problem page and is not part of this claim.

Formalizations. The site's label carries a Lean qualification. Two public Lean 4 developments declare themselves formalizations of the four-point theorem with Juhász as its author: a file posted with the announcement in the problem's forum thread, which names the AI system Aristotle from Harmonic as the author of the formal proof (Lean 4.24.0, Mathlib at the commit its header records), and the file in Alexeev's lean-proofs repository, which carries the same statement and proof under Lean and Mathlib 4.29.1 and names Aristotle and the forum poster as its formal authors. Both are linked above at pinned commits. This corpus has not built or audited either development, so they are links on this page and not evidence of acceptance. The formal-conjectures statement of the problem proves nothing and is not linked here.

Acceptance. The paper is refereed: R. Juhász, Ramsey type theorems in the plane, Journal of Combinatorial Theory, Series A 27 (1979), no. 2, 152–160. The curator of erdosproblems.com, Thomas Bloom, marks the problem proved and credits the result to this paper.