Erdős Problem 654: the Aletheia counterexample
Source: github.com/ukniusanqian-alt/erdos654-lean/tree/3146ec1b4c12…
Lean 4 / Mathlib proof that Erdős Problem 654 has a negative answer: for every m ≥ 10 there is a set of n = 4m points in the Euclidean plane, no four on a circle, in which every point has fewer than 3n/4 distinct distances to the other points. Consequently it is false that every n-point planar set with no four concyclic points has a point with (1 - o(1))n distinct distances. The construction (Aletheia; Feng et al., arXiv:2601.22401) places the points (0, ±3^(k+1)) and (±2^(j+1), 0) on the two coordinate axes.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-03-000009
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-03-000009/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-11-03-000009/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'