Energy minimization for eight points on the sphere

Liudmyla Kryvonos, Lukas Liehr, Mitchell A. Taylor

math.MG Sep 18, 2026 · v1

Read PDF arXiv abstract Code

TL;DR

Computer-assisted proofs that a square antiprism minimizes logarithmic, Coulomb, and Riesz energies of eight points on the sphere are fully verified in Lean.

Abstract

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 large $s$, and a computer-assisted proof that this in fact holds for all $s\geq 0$. We also give examples of energies arising from completely monotonic potentials for which the square antiprism is not a global minimizer, answering in the negative a universality question of Cohn and Woo.

Problem

Determine the configuration of eight points on the unit sphere minimizing discrete Riesz s-energies, including the logarithmic (s=0) and Coulomb (s=1) cases, and characterize all global minimizers up to congruence.

Approach

The optimal member of the square antiprism family is identified via a stationarity equation, then shown globally minimizing by proving a sharp polynomial-minorant energy lower bound and analyzing equality (Gram matrix / moment) configurations. Certificates providing interpolation polynomials and positive definite matrices establish exact identities. The full arguments, including the computer-assisted certificate verification and the counterexample construction, are formalized and verified in Lean.

Results

The unique global minimizer up to congruence for logarithmic and Coulomb energies is a square antiprism with height fixed by a stationarity equation. A Lean-verified non-computer-assisted proof gives optimality for large s, and a computer-assisted proof extends it to all s>=0; counterexamples answer negatively the Cohn-Woo universality question.

N	Configuration	Range
2	Antipodal pair	s>=0
3	Equilateral triangle	s>=0
4	Regular tetrahedron	s>=0
5	Triangular bipyramid	0<=s<=S5
6	Regular octahedron	s>=0

Known optimal configurations by point count

Papers With

Energy minimization for eight points on the sphere