Formally verified AI-led

Erdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateral

A Lean-checked proof that in every two-coloring of the plane, every triangle except possibly one equilateral triangle has a monochromatic congruent copy, settling a 1973 conjecture of Erdős, Graham, Montgomery, Rothschild, Spencer and Straus, found by GPT-6 Astra and Claude Opus 5.5 working in alternation.

Lab: Plasma AI
Model: GPT-6 Astra (Codex) and Claude Opus 5.5 (Claude Code), alternating; Claude Opus 5.5 (Lean formalization)
Field: Mathematics
Date: 2026-10-19
Human collaborators: Jacob Parish
Problem posed: 1973 · open 53 yrs

Sources

Original work

GitHubplasma-ai/erdos-173, the Lean development and AI disclosure↗GitHubBlueprint: the prose proof, written by Claude Opus 5.5 from Plasma AI's write-up↗

What was found

Erdős, Graham, Montgomery, Rothschild, Spencer and Straus conjectured in 1973 that every non-equilateral triangle has a monochromatic copy in every two-coloring of the plane, and gave the alternating-strip coloring that shows one equilateral triangle can be missed. Special cases were settled for right triangles by Shader in 1976, for colorings with closed or open classes by Jelínek, Kynčl, Stolař and Valla in 2009, and for further families by Currier, Moore and Yip in 2024. By the eight-point configuration of the 1975 sequel, it suffices to show that no coloring avoids the equilateral triangles of two different side lengths. The proof does this with a spectral argument for side ratios far from one, an irrational-rotation argument on circles for ratios near one, and a transfer from arbitrary to measurable colorings adapted from OpenAI's unrefereed preprint 'The Euclidean plane is not five-colorable', extended here from the algebraic numbers to the algebraic closure of $\mathbb{Q}(x)$ for every real $x$ . Comparator checks five theorems, three of them, erdos_173 included, copied verbatim from Formal Conjectures.

Novelty check

On 2026-10-20 erdosproblems.com still listed Problem 173 as open with no proof claims, and Formal Conjectures carries it as open. The repository records its own search of 17 October, covering Bloom's entry and thread, the Formal Conjectures issue and pull request, arXiv abstracts on Euclidean Ramsey theory and the openai/math release, which found no proof beyond the special families above; a web search here on 2026-10-20 found nothing further. Erdős and Graham's 1979 statement, which Bloom cites, asks for more, that a single color class contain every triangle but one equilateral, and that stronger form remains open.

Caveats and known objections

Graded formal on the Palomar registration, which replays the proof against Challenge.lean under the three standard axioms with two independent kernels, and on the statement: erdos_173, HasMonochromaticCopy and the Shader and strip-coloring variants are identical, apart from category attributes, to Formal Conjectures' file at commit 7db2ea3b91, written independently of the prover, and the two files' notation for the plane resolves to the same Mathlib type. The two statements that carry the non-equilateral and collinear forms are the authors' own, short and in Mathlib terms; they read as Conjecture 3 states it, but nobody without a stake has confirmed that. The grade certifies the theorem, not the prose: the blueprint was written by Claude Opus 5.5 from Plasma AI's write-up, the only review of the argument was by GPT-6 Astra and did not cover the blueprint or the Lean, and no mathematician is on record as having read it. About two-thirds of the Lean is vendored from openai/math, written by an internal OpenAI model; it builds as part of the project, so the formal grade covers it, but the mathematics it encodes comes from an unrefereed preprint. Autonomy is ai-led rather than autonomous because Plasma AI chose the problem, assembled the research brief that carried the starting route, and directed the formalization.

Independent checks

whataifound.org (statement comparison): Compared Challenge.lean at commit 4a368a65 with Formal Conjectures' ErdosProblems/173.lean at 7db2ea3b: HasMonochromaticCopy, erdos_173 and the right-triangle and equilateral-exception variants are identical apart from category attributes, and Formal Conjectures' plane notation is the same EuclideanSpace type the challenge declares locally. · link ↗

Machine-checked elsewhere

PalomarPALOMAR-2026-10-19-000008

plasma-ai/erdos-173 at 4a368a652753 · checked 2026-10-19

ProvedErdos173.erdos_173Erdos173.erdos_173.variants.right_triangleErdos173.erdos_173.variants.equilateral_exceptionErdos173.erdos_173.variants.non_equilateralErdos173.erdos_173.variants.three_distinct_points

A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.

Permitted axioms are exactly propext, Quot.sound and Classical.choice. Three of the five compared statements are Formal Conjectures' verbatim; the non-equilateral and three-distinct-points variants are the authors' own.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

Entry history (1 event)

2026-10-20AddedEntered the registry graded Formally verified and AI-led.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Graded formally verified for verification and ai-led for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Erdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateral. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-19-erdos-173-monochromatic-triangles

BibTeX

@misc{whataifound-plasmaai-2026-triangles,
  title        = {Erdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateral},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Plasma AI. Verification: Formally verified. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-10-19-erdos-173-monochromatic-triangles}
}

Related findings

Formally verifiedErdős Problem 408: an unconditional normal order for the number of totient iterationsPlasma AI · 2026-10-19 ClaimedHamilton cycles in connected Cayley graphs of polylogarithmic degree, toward the Lovász conjectureIndependent · 2026-09-26 ClaimedHuang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputsAxiom Math · 2026-09-17

combinatorics euclidean-ramsey-theory erdos-problems lean formalization argument

← All mathematics findings in the registry