Unit-distance graphs of dimension four with nine edges
A graph has dimension n when n is the least number such that its vertices can be placed injectively in ℝⁿ with every edge of length one (Erdős, Harary and Tutte). House proved that a graph of dimension four has at least nine edges, and that nine is attained only by K_{3,3}. This project proves the second half in Lean 4, in the form google-deepmind/formal-conjectures states it as erdos_1007.variants.dimension_four_extremal: a graph of dimension four with nine edges and no isolated vertex is isomorphic to K_{3,3}. The proof follows Chaffee and Noble's proof of House's theorem. On the way it…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-23-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-23-000003/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-09-23-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'