{"id":"palomar/PALOMAR-2026-09-23-000003","url":"https://github.com/Dishah3241/Erdos1007/tree/43f89415a6663848a1445effbda8b3abe77b052b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-23-000003-v1.json","repo":"https://github.com/Dishah3241/Erdos1007","tags":["math.CO","math.MG","msc:05C62","msc:52C10","graph-theory","unit-distance-graphs","discrete-geometry","lean"],"score":0,"title":"Unit-distance graphs of dimension four with nine edges","trust":"high","domain":"math.CO","source":"palomar","authors":["Dishant Shah"],"reviews":0,"subject":"math.CO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-23","reactions":{},"formalized":true,"formalizes":[{"title":"Dimension 4 and dimension 5 graphs with minimum edge set","identifier":"https://ajc.maths.uq.edu.au/pdf/64/ajc_v64_p327.pdf","relationship":"formalizes"}]}