{"id":"palomar/PALOMAR-2026-08-08-000001","url":"https://github.com/kim-em/erdos-unit-distance-comparator/tree/be6c2ee4c9fb16fd6bed442b4c361fb10369beb5","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-08-000001-v3.json","repo":"https://github.com/kim-em/erdos-unit-distance-comparator","tags":["math.CO","math.MG","msc:52C10","msc:11R21","discrete-geometry","lean","unit-distance"],"score":0,"title":"kim-em/erdos-unit-distance-comparator","trust":"high","domain":"math.CO","source":"palomar","authors":["Kim Morrison"],"reviews":0,"subject":"math.CO","summary":"Comparator wrapper certifying that the ErdosUnitDistance library proves the literal negation of the uniform-constant form of Erdős's unit-distance conjecture, from a Mathlib-only statement of that negation.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-14","reactions":{},"formalized":true,"formalizes":[{"title":"Integral points on norm-one tori and the Erdős unit-distance exponent","identifier":"https://x.com/__alpoge__/status/2064409100562366543","relationship":"formalizes"}]}