{"id":"arxiv/2609.22077","url":"https://arxiv.org/abs/2609.22077","tags":["math.MG"],"score":0,"title":"Energy minimization for eight points on the sphere","domain":"math.MG","source":"arxiv","authors":["Liudmyla Kryvonos","Lukas Liehr","Mitchell A. Taylor"],"reviews":0,"subject":"math.MG","summary":"We study the energy minimization problem for eight points on the unit sphere. For the logarithmic and Coulomb energies, we show that the unique global minimizer up to congruence is a square antiprism with height characterized by a unique stationarity equation. The proof is computer-assisted and fully verified in Lean. After this, we consider generalizations of the result to other important energies. For the Riesz $s$-energies, we provide a Lean-verified, non-computer-assisted proof that the square antiprism with height depending on $s$ is the unique global minimizer for all sufficiently…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-18","reactions":{}}