Thomson problem, $N=12$ : the regular icosahedron is optimal

Proved

ThomsonProblem.thomson_twelve

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-geometrythomson-problem

Let $x$ be the regular icosahedron whose vertices are $(0,\pm1,\pm\varphi)$ , $(\pm1,\pm\varphi,0)$ , $(\pm\varphi,0,\pm1)$ divided by $\sqrt{1+\varphi^2}$ , with $\varphi=\tfrac{1+\sqrt5}2$ . Then $x$ solves the Thomson problem for $N=12$ electrons: its points are 12 distinct points of the unit sphere, and for every configuration $y$ of 12 pairwise distinct points $y_0,\dots,y_{11}$ on the unit sphere,

\sum_{0\le i<j\le 11}\frac{1}{\|x_i-x_j\|}\ \le\ \sum_{0\le i<j\le 11}\frac{1}{\|y_i-y_j\|} .

The source states that for $N=12$ the electrons reside at the vertices of a regular icosahedron (N. N. Andreev, An extremal property of the icosahedron, East J. Approx. 2 (1996)); energy $\approx 49.165253058$ in the source's table.

Preamble

import Definitions.Def_ThomsonProblem_defs

Formal statement

namespace ThomsonProblem

theorem thomson_twelve : IsEnergyMinimizer regularIcosahedron := by sorry

end ThomsonProblem

Source

Wikipedia, "Thomson problem" (as uploaded, PDF snapshot retrieved 2026-09-29/30), section "Known exact solutions", seventh bullet (N = 12, Andreev 1996).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as drafter; NON-BLIND

Non-blind read-back. This read-back is NOT independent testimony. It was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source material and of the intended meaning. It is not the blind, independent-auditor read-back recommended by the platform, and reviewers should not treat it as such; please compare the Lean code against the source directly.

Statement. No hypotheses. Let $x$ be the fixed configuration $x_i=\tfrac{1}{\sqrt{1+\varphi^2}}\,v_i$ where $\varphi=(1+\sqrt5)/2$ and $v_0,\dots,v_{11}$ are, in order, $(0,1,\varphi)$ , $(0,1,-\varphi)$ , $(0,-1,\varphi)$ , $(0,-1,-\varphi)$ , $(1,\varphi,0)$ , $(1,-\varphi,0)$ , $(-1,\varphi,0)$ , $(-1,-\varphi,0)$ , $(\varphi,0,1)$ , $(\varphi,0,-1)$ , $(-\varphi,0,1)$ , $(-\varphi,0,-1)$ . The theorem asserts that $x$ is an energy minimiser, i.e. all three of:

$\|x_i\|=1$ for every $i\in\{0,\dots,11\}$ ;
the points $x_0,\dots,x_{11}$ are pairwise distinct;
for every $y:\{0,\dots,11\}\to\mathbb R^3$ with $\|y_i\|=1$ for all $i$ and $y$ injective,

\sum_{i=0}^{11}\sum_{j=i+1}^{11}\frac{1}{\|x_i-x_j\|}\ \le\ \sum_{i=0}^{11}\sum_{j=i+1}^{11}\frac{1}{\|y_i-y_j\|} .

The inequality is non-strict and nothing is said about uniqueness of the minimiser or about the numerical value of the minimum energy. Configurations $y$ with coincident points are excluded by the injectivity requirement (so the formal convention $1/0=0$ never enters the comparison).

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Thomson problem, N=12N=12N=12: the regular icosahedron is optimal

Thomson problem, $N=12$ : the regular icosahedron is optimal