{"id":"palomar/PALOMAR-2026-09-30-000012","url":"https://github.com/Pendzoncymisio/kissing-number-lean/tree/2e403b0d1afe84f41a90cb77d926bc31666a8972","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000012-v1.json","repo":"https://github.com/Pendzoncymisio/kissing-number-lean","tags":["math.MG","cs.LO","msc:52C17","msc:05B40","msc:94B65","msc:68V20","lean","discrete-geometry","kissing-number","sphere-packing"],"score":0,"title":"kissing-number-lean","trust":"high","domain":"math.MG","source":"palomar","authors":["Marek Wrzos"],"reviews":0,"subject":"math.MG","summary":"The kissing number of Euclidean 3-space is 12: at most twelve unit balls with disjoint interiors touch a given unit ball, and twelve do. The upper bound follows Musin's extension of the Delsarte linear-programming method. The Delsarte machinery on the sphere (positive-definite zonal kernels up to degree 9 and the LP bound, which by itself gives only 13) is built from scratch, since Mathlib has no spherical harmonics. The lower bound is the cuboctahedron.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"The kissing problem in three dimensions","identifier":"arXiv:math/0410324","relationship":"adapts"}]}