A Lean Proof of the Thomson Problem for Seven Electrons

Problem

The Thomson problem asks where $N$ charges on a sphere end up when they push each other as far apart as they can. Put $N$ points $x_1, \dots, x_N$ on the unit sphere and minimize the Coulomb energy

E(x) = \sum_{i \lt j} \frac{1}{\lVert x_i - x_j \rVert}.

For $N = 7$ the expected answer is the regular pentagonal bipyramid: five points on the equator and one on each pole. Its energy is

E(P) = \tfrac12 + 5\sqrt2 + \frac{5}{2\sin(\pi/5)} + \frac{5}{2\sin(2\pi/5)} = 14.4529774142\ldots

Numerical searches have found this configuration for decades. Proving it means ruling out every other arrangement of seven points, and the space of arrangements is continuous. Rigorous answers are known for only a few small $N$ . $N = 5$ needed a computer-assisted proof (Schwartz), and $N = 8$ was posted on 18 September 2026 (see “What This Contributes” below).

I gave the agents the problem as two fixed Lean statements and asked them to prove both. This is the statement, exactly as Lean sees it:

abbrev R3 := EuclideanSpace ℝ (Fin 3)

def SphereConfig (n : ℕ) : Set (Fin n → R3) :=
  {x | (∀ i, ‖x i‖ = 1) ∧ Function.Injective x}

noncomputable def coulombEnergy {n : ℕ} (x : Fin n → R3) : ℝ :=
  ∑ i : Fin n, ∑ j ∈ Finset.Ioi i, ‖x i - x j‖⁻¹

noncomputable def cyl (ρ θ h : ℝ) : R3 := !₂[ρ * cos θ, ρ * sin θ, h]

noncomputable def pentBipyramid : Fin 7 → R3 := fun i =>
  if (i : ℕ) < 5 then cyl 1 (2 * π * (i : ℕ) / 5) 0
  else if (i : ℕ) = 5 then cyl 0 0 1
  else cyl 0 0 (-1)

theorem thomson_seven :
    ∀ x ∈ SphereConfig 7, coulombEnergy pentBipyramid ≤ coulombEnergy x

theorem thomson_seven_unique :
    ∀ x ∈ SphereConfig 7, coulombEnergy x = coulombEnergy pentBipyramid →
      ∃ (g : R3 ≃ₗᵢ[ℝ] R3) (σ : Equiv.Perm (Fin 7)), ∀ i, x i = g (pentBipyramid (σ i))

Solution

After about 15 hours and 1,270 messages on the message board, the team had a Lean proof of both theorems. The argument splits every configuration by its smallest pairwise inner product $m$ .

The case split by the smallest pairwise inner product: a cap, five slabs and Case 1 — The case split. Every piece is closed by exact arithmetic checked in the Lean kernel.

Case 1, $m \ge -0.90$ . A degree-5 three-point semidefinite-programming bound (of the Bachoc–Vallentin type, adapted to energy problems by Cohn and Woo), with exact integer data checked by kernel evaluation, gives $E \ge E(P) + 3 \times 10^{-4}$ .
Case 2, $m \lt -0.90$ . Five slabs covering $[-0.99, -0.90]$ are each excluded by a three-point certificate, with a margin of about $2.6 \times 10^{-6}$ above $E(P)$ . The remaining cap, $m \le -0.99$ , is handled by a certificate whose bound lies only $2.3 \times 10^{-16}$ below $E(P)$ . That confines any competitor to a thin tube around the bipyramid’s pattern of inner products. An interval-arithmetic rigidity argument and an exact second-order local-minimality theorem then finish the job and give uniqueness.

The two final theorems are short: five lines that glue the cap, the five slabs and Case 1 together.

What This Contributes

This is a complete, machine-checked proof of both halves of the Thomson problem at $N = 7$ : the pentagonal bipyramid has the lowest energy, and every minimizer is that same shape, rotated, reflected or relabeled. Every step is closed by exact arithmetic inside Lean’s kernel, so the result rests on exact computation rather than on floating-point numbers or numerical tables.

The proof builds on the $N = 8$ results posted in September 2026: the computer-assisted, Lean-verified proof by Kryvonos, Liehr and Taylor (arXiv 2609.22077), and the Lean development by Joseph Tooby-Smith and Alex Zughaid, which uses linear-programming and three-point semidefinite-programming bounds (Bachoc–Vallentin, Cohn–Woo). At $N = 7$ the proof combines that method with a case split on the smallest inner product, typed certificates that treat the poles and the equator separately, and an exact second-order argument at the bipyramid that gives uniqueness.

The certificates were found with numerical semidefinite programming and rounded to exact numbers. Lean checks those numbers, so the proof holds independently of the solver that found it.

Formal Verification

The proof is one file, Solution.lean, 17,895 lines, importing Mathlib only. I ran five checks on it:

Check	What it establishes	Result
Lean build from a clean copy	Every step type-checks and every goal is closed	599 s wall clock, of which `lake build` took 344 s (8,928 jobs)
`#print axioms` on both theorems	The proof uses only Lean’s standard axioms	only `propext`, `Classical.choice`, `Quot.sound`
Lean Comparator	The solution proves exactly the fixed challenge statements	”Your solution is okay!” (260 s)
Second kernel (nanoda) on an export	A separate kernel implementation accepts the proof	47,854 declarations, no errors
Negative control	The second-kernel check catches a one-integer change	changing one integer of the Case 1 data makes nanoda abort

Together these show that the proof establishes exactly the statement above.

Elicitation

I deployed ten Claude Sonnet 5.5 agents at maximum effort, gave them a message board and a Lean project, and let them run for about 15 hours. They wrote 1,270 messages.

The brief was specific about the target: kernel-checked Lean against statements fixed in a challenge file, using only Lean’s standard axioms. It proposed nine directions, among them porting the $N = 8$ precedent, linear-programming bounds, splitting by combinatorial type and building a verified certificate engine. The agents were free to drop or merge directions and to say why. One agent claimed the integrator role and inlined the verified pieces into the single solution file.

A candidate proof counted only after it passed the checker: a reproducible Lean build, the Comparator against the fixed challenge file, and an axiom check.

The Lean sources, the paper, the check scripts, an index from the paper to Lean line numbers and the verification logs are at github.com/huwngtran/thomson-n7-lean.