Motivation

The Thomson problem asks for the configuration of $N$ electrons, constrained to the surface of the unit sphere and repelling each other according to Coulomb's law, that minimises the total electrostatic potential energy. J. J. Thomson posed it in 1904 in connection with his "plum pudding" atomic model. The same energy-minimisation question reappears in the arrangement of protein subunits in spherical virus shells, in colloidosomes, in fullerene patterns and in multi-electron bubbles, and it is a special case ($s=1$) of the Riesz $s$-energy problem on the sphere; the logarithmic variant is Smale's 7th problem.

Despite its elementary statement, the minimum is rigorously known only for a handful of values of $N$.

Timeline of exact solutions (as reported in the source).

• $N=1,2$: trivial; for $N=2$ the optimum is an antipodal pair with $U=1/2$.
• $N=3$: equilateral triangle on a great circle — L. Föppl (1912).
• $N=4$: regular tetrahedron (listed in the source without a citation).
• $N=6$: regular octahedron — V. A. Yudin (1992).
• $N=12$: regular icosahedron — N. N. Andreev (1996).
• $N=5$: triangular bipyramid — R. Schwartz (2013), computer-assisted.
• $N=7$: pentagonal bipyramid — long observed numerically; in September 2026 an exact, Lean-kernel-checked proof was claimed (H. Tran, Vals AI).
• $N=8$ and $N=20$: numerically, the optimum is not the cube, resp. the dodecahedron.

Setting

A configuration of $N$ points is a map $x:\{0,\dots,N-1\}\to\mathbb R^3$. It is admissible if every point lies on the unit sphere, $\|x_i\|=1$, and the points are pairwise distinct. In units with $e=1$ and $k_e=1$ its Coulomb energy is

$$U(x)=\sum_{0\le i<j\le N-1}\frac{1}{\|x_i-x_j\|}.$$

An admissible $x$ is an energy minimiser (solves the Thomson problem for $N$) if $U(x)\le U(y)$ for every admissible $N$-point configuration $y$.

Explicit candidate configurations are fixed in the definitions file: the antipodal pair ($N=2$), an equatorial equilateral triangle ($N=3$), the regular tetrahedron ($N=4$), the triangular bipyramid ($N=5$), the regular octahedron ($N=6$), the pentagonal bipyramid ($N=7$: the two poles plus a regular pentagon $(\cos\tfrac{2\pi k}5,\sin\tfrac{2\pi k}5,0)$ on the equator) and the regular icosahedron ($N=12$).

Formalization targets

Goal: $N=7$

$$\text{the pentagonal bipyramid is an energy minimiser for } N=7 .$$

This asserts admissibility of the seven points and the inequality $U(P_7)\le U(y)$ against every admissible seven-point configuration $y$. It fixes no numerical value of the minimum and does not assert uniqueness.

Milestones: the other known exact solutions

$$N=1:\ U\equiv 0;\qquad N=2:\ \text{antipodal pair optimal},\ U=\tfrac12;$$ $$N=3,4,5,6,12:\ \text{triangle, tetrahedron, triangular bipyramid, octahedron, icosahedron are energy minimisers.}$$

Significance

The result. Among the values of $N$ listed in the source, $N=7$ is the smallest one whose optimum was, until the 2026 claim, supported only by numerical computation; the cases $N\le 6$ and $N=12$ were settled earlier. Settling $N=7$ extends the short list of rigorously known Thomson minimisers.

Formalizing it. The $N=7$ result reported in the source is recent and described there as a claimed Lean-kernel-checked proof; a formalization on this platform against a public, reviewed statement would corroborate it independently. For the milestones, the source attributes the $N=3,5,6,12$ cases to published proofs (Föppl 1912, Schwartz 2013, Yudin 1992, Andreev 1996); the source does not describe machine-checked proofs of these, and each is a self-contained formalization target.

Difficulty

The energy is a non-convex function on the configuration space $(S^2)^N$ with many critical points, so numerical minimisation — which is how most entries of the source's table of smallest known energies were obtained — does not certify global optimality. The $N=5$ case, the most recent classical entry before $N=7$, was resolved only with a computer-assisted proof (Schwartz 2013).

Formalization scope

Points live in EuclideanSpace ℝ (Fin 3); configurations are functions Fin N → EuclideanSpace ℝ (Fin 3). Admissibility requires unit norm and injectivity (distinct points), matching the source's "$N$ distinct points". The energy sums $1/\mathrm{dist}(x_i,x_j)$ over $i<j$; Lean's $1/0=0$ convention is harmless because coincident points are excluded by admissibility. The candidate configurations are fixed in one particular orientation; since the energy is invariant under orthogonal maps and relabelling, this is no loss of generality. The statement "$x$ is an energy minimiser" includes admissibility of $x$ itself, so the goal cannot be satisfied by a degenerate candidate.

Reusable infrastructure welcome: energy invariance under isometries and permutations, existence of minimisers by compactness, linear-programming (Delsarte–Yudin) bounds on the sphere, and interval-arithmetic tooling for certified numerical bounds.

Selected references

• Wikipedia, Thomson problem (source of this mission). https://en.wikipedia.org/wiki/Thomson_problem
• J. J. Thomson, On the Structure of the Atom…, Philosophical Magazine 7 (1904), 237–265.
• L. Föppl, Stabile Anordnungen von Elektronen im Atom, J. Reine Angew. Math. 141 (1912), 251–301. https://doi.org/10.1515/crll.1912.141.251
• V. A. Yudin, The minimum of potential energy of a system of point charges, Discrete Math. Appl. 3 (1993), 75–81. https://doi.org/10.1515/dma.1993.3.1.75
• N. N. Andreev, An extremal property of the icosahedron, East J. Approx. 2 (1996), 459–462.
• R. Schwartz, The five-electron case of Thomson's problem, Experimental Mathematics 22 (2013), 157–186. https://arxiv.org/abs/1001.3702
• S. Smale, Mathematical Problems for the Next Century, Math. Intelligencer 20 (1998), 7–15. https://doi.org/10.1007/bf03025291
• Vals AI, A Lean Proof of the Thomson Problem for Seven Electrons (2026). https://www.vals.ai/blogs/thomson-n7-lean-proof