---

Claim. For every two-coloring $c:\mathbb R^2\to\{-1,1\}$ of the plane, with no measurability or other regularity assumed, there is at most one positive length $r$ such that $c$ has no monochromatic equilateral triangle of side $r$. Equivalently, for every real $x>0$ with $x\ne1$, every two-coloring of the plane contains a monochromatic equilateral triangle of side $1$ or of side $x$. Under every two-coloring, every set of three distinct points that is not equilateral, collinear triples included, has a monochromatic congruent copy, obtained by a translation and a rotation. Hence for all but at most one triangle $T$ there is a monochromatic congruent copy of $T$, and an exceptional $T$, if there is one, is equilateral, with a side that depends on the coloring.

Submission note. The Palomar registry's description of entry PALOMAR-2026-10-19-000008, registered on 19 October 2026 by a maintainer of the repository, whose formalization.yaml names Jacob Parish and Andrew Turner as its responsible maintainers:

A Lean proof that in every two-coloring of the plane any three distinct points that are not the vertices of an equilateral triangle, collinear points included, have a monochromatic congruent copy and at most one equilateral side length is missed, so at most one triangle up to congruence, degenerate or not, has no monochromatic copy. Alternating strips show that one equilateral triangle can be missed. This answers Erdős Problem 173 as Bloom states it and settles the conjecture of Erdős, Graham, Montgomery, Rothschild, Spencer and Straus that every non-equilateral triangle has a monochromatic copy, collinear triples included; it is new to our knowledge. The step from arbitrary to measurable colorings adapts OpenAI's rigidity theorem for wild character laws, extended here from the algebraic numbers to the algebraic closure of ℚ(x) in ℂ for every real x, and its transfer from proper to weak measurable colorings.

Covers. The whole Statement of Problem 173, whether or not three distinct collinear points are counted as a triangle. The one exception is needed: as the problem page records, the coloring of the plane by alternating strips has no monochromatic equilateral triangle of one side length. The claim does not classify the colorings that miss an equilateral side length.

Credit. The reduction to two equilateral side lengths is Lemma 1.3 and Corollary 1.4 of Jelínek, Kynčl, Stolař and Valla, who take it from Erdős, Graham, Montgomery, Rothschild, Spencer and Straus; the two-scale lead reconstructs its eight-point configuration in coordinates. The rigidity and transfer steps build on OpenAI's manuscript The Euclidean plane is not five-colorable (OpenAI Math Release, September 23, 2026), whose subject is the chromatic number of the plane. Its Sections 2 and 3 give a proof that every wild rotation-invariant character law on the algebraic plane is Haar measure, using a selection step confined to number fields, and its Lemma 4.1 and Proposition 4.2 transfer proper colorings to weak measurable ones by projection onto the continuous vectors. Plasma AI supplies the rest. At algebraic ratios the manuscript's number-field step applies as stated; at transcendental ratios a function-field finite-cover theorem gives the unit-vector template that replaces it. With that template, the manuscript's other lemmas, their field hypotheses checked for the new field, extend its rigidity theorem to $F_x(i)$, where $F_x$ is the real closure of $\mathbb Q(x)$ in $\mathbb R$, for every real $x>0$. Plasma AI also proves that the two-scale question on that countable field is equivalent to the whole-plane question, adapts the manuscript's projection to two colors and three-point configurations by thresholding the quadratic $1+ab+ac+bc$, excludes two unequal scales for measurable colorings by a Bessel bound for $x\ge3/2$ or $x\le2/3$ and a circle argument inside that window, and composes these into the whole conclusion. The circle argument uses the Lebesgue density theorem and Federer's criterion for finite perimeter (H. Federer, Geometric Measure Theory, 1969, 4.5.11), the latter checked at statement level. Neither the manuscript's five-color theorem nor its Lean formalization is a premise. Two AI models found Plasma AI's proof on October 16 and 17, 2026, working in alternating steps: GPT-6 Astra in Codex and Claude Opus 5.5 in Claude Code, as the formalization repository's README records.

Formalization. The repository plasma-ai/erdos-173 formalizes the result in Lean 4 (v4.35.0-rc3, Mathlib v4.35.0-rc3) at commit 4a368a6, with a prose blueprint that follows the development; its source card digests both. Challenge.lean states five theorems. Three copy formal-conjectures' statement of Problem 173 at its commit of 2026-10-14, verbatim apart from their attribute lists: Erdos173.erdos_173, that any two triangles without a monochromatic congruent copy are congruent, with its variants right_triangle and equilateral_exception. Two are the repository's own: Erdos173.erdos_173.variants.non_equilateral, that every non-equilateral triangle has a monochromatic congruent copy, and Erdos173.erdos_173.variants.three_distinct_points, the same for any three distinct points that are not the vertices of an equilateral triangle, collinear ones included. Triangles in the first four are Mathlib's Affine.Triangle, with affinely independent vertices, and in all five a copy may be reflected and relabelled. Solution.lean proves the five, and comparator.json permits only propext, Quot.sound and Classical.choice. The rigidity step uses the Lean form of OpenAI's theorem from openai/math, generalized over a carrier field with the template property, which the formalization proves for the algebraic closure of $\mathbb Q(x)$ at every transcendental $x$; the circle argument replaces Federer's criterion by an elementary argument with nested squares. The repository's formalization.yaml names Jacob Parish as the formalization's author and records that it was written with Claude Code. The repository is registered on the Palomar registry as PALOMAR-2026-10-19-000008, version 1, first registered on 19 October 2026 (the record link; trust level high, automated review outcome neutral), and the entry pins commit 4a368a6.

Acceptance. Formalized. This corpus rebuilt the formalization, held as the repository's tree at 4a368a6, at its own pinned toolchain, leanprover/lean4:v4.35.0-rc3 with Mathlib at v4.35.0-rc3, in a sandbox with no network. Comparator, run before anything else built the solution, accepted the five theorems against Challenge.lean; the kernel replayed, from an empty environment, every declaration each of the five depends on; and each depends only on propext, Classical.choice and Quot.sound (the replay receipt, 2026-10-19). The graded fresh-context review of the statements, by a reviewer and a distinct grader, both agents working from fresh contexts, found all five faithful. erdos_173 covers the Statement for triangles of three non-collinear points, the reading of formal-conjectures and of Mathlib's Affine.Triangle, and three_distinct_points covers any three distinct points, collinear ones included, so the coverage of the Statement is whole whether or not three distinct collinear points count as a triangle. non_equilateral and three_distinct_points state that every set of three distinct points that is not equilateral has a monochromatic copy, so an exceptional triangle is equilateral, and equilateral_exception states that the exception occurs. Acceptance rests on the replay and that review and covers the Statement under either reading. The compared statements allow reflected copies; the claim's assertion that a copy is found by a translation and a rotation alone rests on the tier-1 review below. Jacob Parish at Plasma AI signed off on 2026-10-18 UTC on the basis of the tier-1 review of the whole conclusion and of a replay and graded statement review of an earlier commit of the formalization, which compared three theorems, and on 2026-10-19 approved this acceptance of its five theorems. No referee or reviewer outside the project has examined the proof.

Standing. Tier 1. The lead's whole-conclusion independent examination, with verdict refutation-failed, and its separate passing grade examined this exact conclusion on 2026-10-17 UTC: arbitrary two-colorings, every real ratio $x\ne1$ and collinear triples of distinct points. The reviewer and the grader, both GPT-6 Astra agents working from fresh contexts, are distinct from the authors and from each other; GPT-6 Astra is also one of the models that found the proof, and the grade rules that model identity is not the basis of their independence. The examined argument includes, as proof, the deductions it uses from the manuscript's Sections 2 and 3 and its Section 4 interfaces, read as text and not checked against the printed edition. The warrant does not extend to the manuscript's other results or its Lean formalization, to the original proofs of the classical theorems used, such as Federer's criterion, or to novelty; the source-access account records the editions and these boundaries. A retained exact-arithmetic program checks the finite rational inequalities of the Bessel bound; every other step is proof. The review's subject is the seven-step argument on the two-scale lead, with the parts of its finite-cover, rigidity-extension, carrier, binary-transfer, spectral and circle accounts that it uses. The Lean proof is external, not in this repository's Lean closure, so it confers no tier 2.

Depends on. The formalized main theorem, whose proof uses OpenAI's spectral rigidity theorem in its Lean form. For copies by a translation and a rotation alone, the two-scale lead (tier 1), whose seven-step proof is the subject of the whole-conclusion review. No native claim card is a premise.