Six concyclic points satisfy the Euclidean Ramsey tensor criterion, as does every spherical set of at most m + 4 points of affine dimension m and every algebraic spherical set; given the classification's sufficiency half, these sets are Ramsey (the algebraic ones when spanning)
A Lean 4 development around the tensor criterion of the classification of finite Euclidean Ramsey configurations (openai/math, family 172). With the criterion's definitions restated character for character from that project's challenge file: every set of six distinct points on a circle satisfies the criterion, by an explicit certificate (the product of the two bilinear forms through the first three and the last three points of a homogeneous parametrisation of the circle, scaled and conjugated by the parametrisation); the sharp dimension theorem: every spherical set of at most m + 4 distinct…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-07-000011
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-07-000011/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-07-000011/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'