Erdős Problem 173: monochromatic triangles in two-colorings of the plane

This Lean 4 project proves the statement of Erdős Problem 173, as cataloged by Thomas F. Bloom: in every two-coloring of the plane, every triangle with at most one exception has a monochromatic congruent copy. More precisely, we prove

• any three distinct points that are not the vertices of an equilateral triangle, collinear points included, have a monochromatic congruent copy in every two-coloring of the plane, and
• no two-coloring of the plane misses the monochromatic equilateral triangles of two different side lengths.

So a two-coloring misses at most one triangle up to congruence, counting three distinct collinear points as a degenerate triangle, and that triangle is equilateral. The exception can occur: alternating half-open strips of width √3/2, the coloring of Euclidean Ramsey theorems, I, contain no monochromatic equilateral triangle of side one. The colorings are arbitrary; no measurability is assumed. A copy may be reflected and relabelled, as in the problem, though the proof finds copies by translation and rotation alone.

To our knowledge, this result is new. It settles the conjecture of Erdős, Graham, Montgomery, Rothschild, Spencer and Straus that every non-equilateral triangle has a monochromatic copy in every two-coloring of the plane, collinear triples included, and it answers Erdős Problem 173 as Bloom states it. In the terms of Euclidean Ramsey theorems, III, the compared theorem erdos_173 settles their Conjecture 2, that a coloring missing the equilateral triangle of one side has those of every other side, from which their Theorem 1 gives Conjecture 3, on non-equilateral triangles. The development does not formalize Theorem 1 as such, only the direction of it that the proof uses: by part (i) of the eight-point configuration, which holds for collinear points too, a coloring with no monochromatic copy of three distinct points has no monochromatic equilateral triangle of any of their side lengths. erdos_173.variants.non_equilateral compares Conjecture 3 directly for nondegenerate triangles, and erdos_173.variants.three_distinct_points compares it for any three distinct points, collinear ones included. Erdős and Graham's statement of the problem (L'Enseignement Math. 25, 1979, p. 330), which Bloom cites, asks for more: that a single color class contain a copy of every three-point set with the possible exception of one equilateral triangle. That stronger form remains open.

Comparator checks five theorems. Three are copied verbatim, apart from their category attributes, from formal-conjectures: the problem itself (erdos_173), Shader's right-triangle theorem (erdos_173.variants.right_triangle), and the existence of an exceptional equilateral triangle (erdos_173.variants.equilateral_exception). The other two are not from formal-conjectures: erdos_173.variants.non_equilateral states that every non-equilateral triangle has a monochromatic congruent copy, and erdos_173.variants.three_distinct_points states the same for any three distinct points that are not the vertices of an equilateral triangle, collinear points included.

Literature and scope

Erdős, Graham, Montgomery, Rothschild, Spencer and Straus first stated the conjecture in Euclidean Ramsey theorems, I (J. Combin. Theory Ser. A 14, 1973, p. 347), where they also gave the strip coloring (p. 342). In Euclidean Ramsey theorems, III (Infinite and Finite Sets, Colloq. Math. Soc. János Bolyai 10, 1975, 559–583) they restated it as Conjectures 2 and 3, in a form that includes collinear triples, and proved it for several families of triangles. Their Theorem 1 reduces the problem to equilateral triangles: a coloring misses a triangle with sides a, b, c exactly when it misses the equilateral triangles of all three sides. Shader, All right triangles are Ramsey in E²! (J. Combin. Theory Ser. A 20, 1976, 385–389), proved the conjecture for right triangles. Jelínek, Kynčl, Stolař and Valla, Monochromatic triangles in two-colored plane (Combinatorica 29, 2009), proved it for colorings whose classes are closed and open, and for polygonal colorings. Currier, Moore and Yip, Any two-coloring of the plane contains monochromatic 3-term arithmetic progressions (Combinatorica 44, 2024), settled further families, including degenerate ones. Graham's survey chapter Euclidean Ramsey theory (Handbook of Discrete and Computational Geometry, 3rd edition, 2017) states the conjecture as Conjecture 11.1.1. Its stronger Conjecture 11.1.2, that a single class of every two-coloring contains every triangle with the possible exception of one equilateral triangle, is not addressed here.

The "to our knowledge" novelty claim reflects a targeted search on October 17, 2026 of Bloom's problem entry (listed as open, with no proof claims) and its discussion thread, the formal-conjectures issue (#403) and pull request (#6686) for the problem, arXiv abstracts on monochromatic triangles and Euclidean Ramsey theory in two-colorings of the plane, the openai/math preprint release, and the web. That search found no proof of the conjecture beyond the special families above.

The step from arbitrary to measurable colorings adapts two results of OpenAI's The Euclidean plane is not five-colorable (23 September 2026), an unrefereed preprint produced by an OpenAI model, and their Lean formalization: the rigidity theorem for wild character laws (Theorem 2.3) and the transfer from proper to weak measurable colorings (Lemma 4.1 and Proposition 4.2). The rigidity theorem is stated over the field of algebraic numbers. This project extends it to the algebraic closure of ℚ(x) in ℂ for every real x, which is what makes transcendental ratios of side lengths accessible.

The proof is Plasma AI's, building on the reduction of Erdős et al. in the form of Jelínek et al.'s Lemma 1.3, and on OpenAI's rigidity theorem for wild character laws (Theorem 2.3) and its transfer from proper to weak measurable colorings (Lemma 4.1 and Proposition 4.2). Two AI models found it on October 16 and 17, 2026, working in alternating steps: GPT-6 Astra in Codex and Claude Opus 5.5 in Claude Code. An internal independent review and a separate grade, both by GPT-6 Astra, passed the argument; they did not cover the blueprint or the Lean. The blueprint, written by Claude Opus 5.5 in Claude Code from Plasma AI's write-up of the proof, is its first public presentation and states it in prose, following the Lean development module by module. Claude Opus 5.5 wrote the Lean formalization in Claude Code under human direction, apart from the vendored OAI/ library, about two-thirds of the Lean, which an internal OpenAI model wrote for openai/math. The project lead checked the three formal-conjectures statements in Challenge.lean against the problem; the other two have not had that check. formalization.yaml records the role of each model.

The argument

By the eight-point configuration of Lemma 1.3 of Jelínek et al. (taken from Erdős et al.), a monochromatic equilateral triangle of side a forces a monochromatic copy of every triangle with a side a, collinear triples of distinct points included. So it suffices to show that no coloring avoids the equilateral triangles of two sides, and after rescaling, of sides 1 and x ≠ 1.

The label model. Restrict an avoiding coloring to a countable dense subfield L of ℂ containing x, closed under conjugation and relatively algebraically closed. Its labelings of L with no monochromatic equilateral triangle of side 1 or x form a compact space, and OpenAI's stationary mean gives it an invariant probability measure under translations by L and rotations by the unit circle of L. OpenAI's rigidity theorem for wild character laws says that a rotation-invariant law on the characters of L that gives no mass to the continuous characters is Haar measure. For the sign f of the origin it gives ⟪f, T_z f⟫ = ⟪P f, T_z P f⟫ for z ≠ 0, where P is OpenAI's projection onto the vectors continuous under translation.

Far ratios. Three signs that are not all equal have pair products summing to -1, so the correlation at distances 1 and x is -1/3. The spectral measure of f on the ordinary characters gives a radial measure ν of mass at most one with ∫ J₀(t) dν = ∫ J₀(x t) dν = -1/3. This is impossible when x ≥ 3/2 or x ≤ 2/3, since then J₀(t) + J₀(x t) ≥ -83/125 > -2/3. The bound is proved from rational enclosures of the power series of J₀ and J₁ at finitely many points, the Lipschitz bound on J₁, and the decreasing energy J₀² + J₁².

Binary transfer. For two colors on a triangle, 1 + ab + ac + bc vanishes exactly on the non-monochromatic sign triples and is nonnegative on [-1, 1]³. It involves only pair products, which the projection preserves, so the continuous field P f, sampled at one labeling and thresholded at zero as in OpenAI's transfer, is a measurable coloring with almost no monochromatic equilateral triangle of side 1 or x.

Ratios near one. For 2/3 < x < 3/2, x ≠ 1, one of the apex angles γ of the isosceles triangles with sides 1, 1, x and x, x, 1 is an irrational multiple of π (a cyclotomic argument); let r be its leg. Call the set of points where neither color has density zero the boundary; it is null by Lebesgue's density theorem. At a boundary point, the circle of radius r either meets the boundary in positive length, or its red density points R satisfy R + π/3 = Rᶜ and R + γ = Rᶜ up to null sets, which irrational rotation makes impossible. So the null boundary supports itself on circles, and the map (θ, φ) ↦ p + r e^{iθ} + r e^{iφ} then gives it positive area unless it is empty. It is not empty: nested squares in which red has proportion exactly one half shrink to a point where both colors have positive upper density.

The carrier. The rigidity theorem's proof uses the number field structure of the algebraic numbers in exactly one step, a selection of unit vectors whose rational span contains 1 and i. Every other step uses only that the carrier is countable, dense, relatively algebraically closed and the complexification of its real slice. The development isolates that step as the template property of the carrier. For algebraic x the carrier is the field of algebraic numbers, where OpenAI's number-field general position (Lemma 3.4) gives the template property. For transcendental x it is the algebraic closure L of ℚ(x), and the template property is proved here: a finite cover of the unit group of L by translated kernels of a functional linear over the algebraic numbers would force rational Cauchy transforms in a finite extension of ℚ̄((x + i)/(x - i)), then a finite-dimensional quotient algebra, in which Cayley transforms rule out the cover, by a generalization of OpenAI's algebraic Cayley lemmas. A compactness argument on the space of choices and OpenAI's number-field general position turn this into the template property with rational coefficients.

Publication layout

Challenge.lean states the five theorems using only Mathlib imports. Its five sorry proofs are deliberate: this file contains the statements to audit. HasMonochromaticCopy and three of the statements are copied verbatim, apart from their category attributes, from formal-conjectures (FormalConjectures/ErdosProblems/173.lean, commit 7db2ea3b91), with its ℝ² notation for EuclideanSpace ℝ (Fin 2) declared locally; the other two, erdos_173.variants.non_equilateral and erdos_173.variants.three_distinct_points, are not from formal-conjectures. A triangle in the first four is Mathlib's Affine.Triangle, whose vertices are affinely independent, so collinear triples are not covered there; erdos_173.variants.three_distinct_points is stated for any three distinct points, so it covers them. In every statement a copy may be reflected and relabelled. Solution.lean imports the proof development and supplies the five theorems. comparator.json selects their names and the allowed axioms for Comparator.

The proof development lives under Erdos173/:

• Statement.lean repeats HasMonochromaticCopy for the development. Basic.lean defines colorings of ℂ, monochromatic copies of a triangle template (0, a, b), and avoidance and weak (almost everywhere) avoidance.
• Reduction/ holds the eight-point configuration, part (i) pointwise and part (ii) in measure form (EightPoint.lean), the identification of ℝ² with ℂ and of three distinct points, collinear or not, with templates (Plane.lean), and the strip coloring (Strips.lean).
• Bessel/ proves J₀(t) + J₀(x t) ≥ -83/125 for x ≥ 3/2.
• Transfer/ builds the label model over a carrier, its radial spectral measure, the exclusion of far ratios, and the binary transfer.
• Measurable/ proves the circle exclusion of ratios near one for measurable colorings.
• Template/ proves the template property of the algebraic closure of ℚ(x) for transcendental x.
• TwoScale.lean chooses the carrier and combines the two exclusions, and FinalAssembly.lean derives the five theorems.

Three of these files adapt code from openai/math: Template/CayleyEscape.lean generalizes its algebraic Cayley lemmas from ℚ to a base field K, Transfer/LabelModel.lean adapts its label model, and Transfer/Sample.lean its projected color vectors.

OAI/ holds 34 modules from the lean/ directory of openai/math at commit adc7f1241b42e322a6451854ab7e4b4c146bf78a, under its Apache 2.0 license (OAI/LICENSE), and two new modules. As recorded upstream, an internal OpenAI model wrote the 34. They are the import closure of OAI.Analysis.PlaneSpectrum.Ergodicity, OAI.Analysis.PlaneSpectrum.CircleDecay, and OAI.Geometry.PlaneColoring.BorelTransfer, under their upstream module names, ported to this toolchain and the module system. They are generalized from the algebraic numbers to any carrier field with the template property: the new module PlaneSpectrum/Carrier.lean defines the class Carrier of carrier fields (countable, relatively algebraically closed, the complexification of its real slice F, with the template property) and the fields fieldOf x and realFieldOf x, the algebraic closures of ℚ(x) in ℂ and ℝ; the modules that depend on the carrier take a [Carrier] argument; and the new module PlaneSpectrum/Carriers.lean defines the two carriers, algebraicCarrier, whose template property follows from the source's number-field general position, and carrierOf x h, the algebraic closure of ℚ(x) given its template property h. OAI/README.md records their provenance and every change, and each changed file begins with a comment pointing to it.

Every Lean file uses the module system: it begins with module, imports with public import, and exposes its definitions with @[expose] public section. The only options set in the Lean sources are two raises of synthInstance.maxHeartbeats, in OAI/Analysis/PlaneSpectrum/SpectralMeasure.lean and Erdos173/Template/Cover.lean.

blueprint/proof.md states the proof in prose, section by section along the development, naming the Lean declarations of each step, and records where the Lean route departs from Plasma AI's original write-up.

formalization.yaml records the mathematical sources, authorship, AI use, source fidelity, and review status for a registry submission.

The Lean and Mathlib versions are fixed by lean-toolchain, lakefile.toml, and lake-manifest.json.

lake exe cache get
lake build

The full build includes Challenge and therefore reports its intentional sorry warnings. The proofs in Solution can also be built directly with lake build Solution.