Thomson problem, $N=7$ : the pentagonal bipyramid is optimal

Proved

ThomsonProblem.thomson_seven

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

discrete-geometrythomson-problem

Let $x$ be the pentagonal bipyramid: the poles $(0,0,\pm1)$ together with the regular pentagon $p_k=(\cos\tfrac{2\pi k}{5},\sin\tfrac{2\pi k}{5},0)$ , $k=0,\dots,4$ , on the equator. Then $x$ solves the Thomson problem for $N=7$ electrons: its points are 7 distinct points of the unit sphere, and for every configuration $y$ of 7 pairwise distinct points $y_0,\dots,y_{6}$ on the unit sphere,

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

Computational solutions have long returned the pentagonal bipyramid for $N=7$ (energy $\approx 14.452977414$ in the source's table). The source reports that in September 2026 an exact, Lean-checked proof of this was claimed (H. Tran, Vals AI). This is the goal theorem of the mission.

Preamble

import Definitions.Def_ThomsonProblem_defs

Formal statement

namespace ThomsonProblem

theorem thomson_seven : IsEnergyMinimizer pentagonalBipyramid := by sorry

end ThomsonProblem

Source

Wikipedia, "Thomson problem" (as uploaded, PDF snapshot retrieved 2026-09-29/30), section "Known exact solutions", paragraph on N = 7 (Tran, Vals AI, September 2026 — claimed).

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_0=(0,0,1)$ , $x_1=(0,0,-1)$ , and $x_{2+k}=\big(\cos(2\pi k/5),\sin(2\pi k/5),0\big)$ for $k=0,1,2,3,4$ . The theorem asserts that $x$ is an energy minimiser, i.e. all three of:

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

\sum_{i=0}^{6}\sum_{j=i+1}^{6}\frac{1}{\|x_i-x_j\|}\ \le\ \sum_{i=0}^{6}\sum_{j=i+1}^{6}\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=7N=7N=7: the pentagonal bipyramid is optimal

Thomson problem, $N=7$ : the pentagonal bipyramid is optimal