{"id":"palomar/PALOMAR-2026-10-16-000018","url":"https://github.com/wstrinz/algebraic-plus-three-ramsey/tree/fe257eca4be0d753839b7431b7ea142e47e48d4c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000018-v1.json","repo":"https://github.com/wstrinz/algebraic-plus-three-ramsey","tags":["math.CO","math.MG","msc:05D10","msc:52C10","euclidean-ramsey","discrete-geometry","algebraic-points","lean-formalization"],"score":0,"title":"Algebraic points on a circle plus at most three arbitrary points are Euclidean Ramsey","trust":"high","domain":"math.CO","source":"palomar","authors":["Will Strinz"],"reviews":0,"subject":"math.CO","summary":"Theorem B(b): finitely many distinct points on a circle in the Euclidean plane (centre and radius arbitrary reals), all of whose coordinates are algebraic over Q except for the points with indices in a set T of at most three, form a Euclidean Ramsey configuration. Ramsey is OpenAI's definition from result 172 (for every r >= 2 there is D such that every r-colouring of R^D contains a monochromatic congruent copy). The theorem is stated in OpenAI's vocabulary and again in Mathlib vocabulary (Mathlib's Congruent). With the Möbius invariance of the Ramsey property (mobius-ramsey, Theorem C; the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true}