spherical-codes

The Tammes problem for fifteen points: the optimal minimal distance of 15 points on the sphere, with the reduction proved in Lean 4 with Mathlib

Proof of Cohn and Rajagopal's Conjecture 3.1: six-dimensional kissing configurations containing Q5 or R5 have at most 70 points. Manuscript and exact verification.