{"id":"palomar/PALOMAR-2026-09-30-000026","url":"https://github.com/Dishah3241/FKSProblem2/tree/11413860db107522485d4e8e580ae406363c1164","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000026-v1.json","repo":"https://github.com/Dishah3241/FKSProblem2","tags":["math.CO","math.MG","msc:05C62","msc:52C10","discrete-geometry","unit-distance-graphs","lean-formalization"],"score":0,"title":"FKS Problem 2 in dimension three","trust":"high","domain":"math.CO","source":"palomar","authors":["Dishant Shah"],"reviews":0,"subject":"math.CO","summary":"A Lean-checked proof of the d = 3 case of FKS Problem 2: for every simple graph G on seven vertices, G or its complement has an injective placement in Euclidean three-space under which every edge has length 1. Non-edges are unconstrained and may also have length 1. The full question, for graphs on 2d + 1 vertices in dimension d, is stated and marked open. In the notation of Alon and Kupavskii, the proved case gives f_D(7) ≤ 3; together with the published lower bound it implies f_D(7) = 3. The formal target is the seven-vertex disjunction, not a definition or equality for f_D. The research…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"Embedding graphs in Euclidean space","identifier":"https://arxiv.org/abs/1802.03092","relationship":"formalizes"}]}