The problem

Place $N$ distinct points $x_1,\dots,x_N$ on the unit sphere in $\mathbb{R}^3$ to minimise the Coulomb energy

Good configurations are easy to find numerically, but proving that one is the global minimum is hard. Rigorous proofs exist for only a few $N$:

• $N = 2, 3$: classical.
• $N = 4, 6, 12$: the Delsarte–Yudin linear-programming bound is exact (Yudin; Andreev; Cohn–Kumar).
• $N = 5$: Schwartz, by a large computer-assisted search.
• $N = 8$: Kryvonos–Liehr–Taylor; in Lean by Tooby-Smith–Zughaid.
• $N = 7$: a Lean-verified proof by Hung Tran (package, write-up).

This mission

• $N = 10$ (capped square antiprism) and $N = 9$ (tricapped trigonal prism) are stated as "some member of this one-parameter symmetric family is a global minimiser over all configurations", because the optimal parameter has no known closed form. No symmetry is assumed of competing configurations, and uniqueness is not required. $N = 10$ comes first: like $N = 7$ it has an antipodal pair of poles, which makes the case split easier.
• $N = 32$ (an icosahedron nested with its dual dodecahedron) is the challenge. It is the numerically best-known configuration, but the standard bounds do not close the gap there, so a new idea is needed.

The shared lemmas (the distance formula, two-point positivity behind the Delsarte–Yudin bound, and three-point positivity behind the Bachoc–Vallentin and Cohn–Woo bounds) are stated once for reuse, along with well-posedness of each configuration.