# Thomson N=7: ten agents, 17,895 lines of Lean, one trusted kernel

> Satyajit Ghana — Head of Engineering @ Inkers Technology
> canonical: https://ai.thesatyajit.com/articles/thomson-n7-lean
> date: 2026-10-02
> tags: formal-methods, theorem-proving, agents, verification, llm, explainer

Put seven equal point charges on a sphere, let them repel, and ask where they come to rest.
For decades the computer answer has been the same: a **pentagonal bipyramid** — five charges on
the equator, one at each pole. Computed, never proved. The N=7 case of the Thomson problem sat in a
strange gap: small enough that any numerical search finds the answer in a second, but with no
rigorous proof that the bipyramid is actually the global minimum and not just a very good local one.

That gap closed in late September 2026. Vals AI put **ten Claude Sonnet 5.5 agents** on the problem,
and in about **15 hours** — across **1,270 messages** on a shared board — they produced a
**17,895-line Lean 4 proof** that the pentagonal bipyramid is the unique minimiser, which Lean's
kernel accepted. The code, a paper, and the verification logs are in a public repository,
[`huwngtran/thomson-n7-lean`](https://github.com/huwngtran/thomson-n7-lean). I cloned it and checked
the claims I could without a 14 GB Lean build. The numbers hold. The caveats are real, and I will
not bury them: the repo has no license, it is not peer reviewed, and its own description says
*"Statement not human-certified."* More on what that last phrase means at the end — it is the part
that matters most.

## The Thomson problem, and why seven is the hard one

Write the configuration as seven distinct unit vectors $x_1,\dots,x_7$ on the sphere $S^2$. The
energy is the sum of inverse distances over unordered pairs:

$$E(x) = \sum_{i<j} \lVert x_i - x_j \rVert^{-1}.$$

Minimising $E$ is easy to state and brutal to prove, because a minimiser has to beat *every* other
arrangement — an uncountable space of them. Global-optimality proofs exist for only a handful of
$N$. The cases $N \le 4$, $N = 6$ and $N = 12$ fall out of the universal-optimality theory of
Cohn and Kumar (2007): the regular simplex, octahedron and icosahedron are optimal for *every*
reasonable repulsive potential at once. $N = 5$ was settled by Schwartz in 2013, with an ad-hoc
computer-assisted argument using interval arithmetic — a proof it was not even obvious could be
formalised. And $N = 8$ was done only weeks earlier, in work by Kryvonos, Liehr and Taylor
([arXiv:2609.22077](https://arxiv.org/abs/2609.22077), 18 Sep 2026), with a Lean development by
Tooby-Smith and Zughaid. The N=7 proof adapts that machinery one case down.

Seven is awkward for a reason you can see. The optimal shapes for 6 and 12 are Platonic solids: one
orbit of vertices, every point equivalent, enormous symmetry to exploit. The pentagonal bipyramid is
not like that. It has **two kinds of vertex** — the two poles and the five equatorial points — and
they are genuinely different: a pole sits at distance 2 from the other pole and $\sqrt 2$ from every
ring point, while a ring point has two neighbours and two diagonals at two different distances. In
inner-product terms, the 21 pairwise values $\langle x_i, x_j\rangle$ take four values: $-1$ once,
$0$ ten times, and two irrational numbers $c_1 = \tfrac{\sqrt5 - 1}{4} \approx 0.309$ and
$c_2 = -\tfrac{\sqrt5 + 1}{4} \approx -0.809$ five times each. Any proof has to respect that
two-orbit structure, and that is exactly where the N=7 argument spends its effort.

<SphereRelax />

The minimum energy is $E(P) = 14.4529774142\ldots$ — to full precision $14.45297741422134$, worked
out in closed form in the paper and reproduced in the Lean file to 40 digits as

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

That is the number the whole proof is organised around: every certificate's job is to show
$E(x) \ge E(P)$ for its slice of configurations, with equality only at the bipyramid itself.

## What "machine-checked" actually buys you

Formal theorem proving is one of the few corners of this field where correctness is not a matter of
taste. A proof in [Lean 4](https://leanprover.github.io/) is a term whose type is the statement;
either Lean's small, fixed kernel can re-derive that term from the axioms, or it cannot. There is no
partial credit and no persuasive prose. Lean's kernel is a few thousand lines that have been stared
at for years, and `Mathlib` — the community library this proof builds on, pinned here to commit
`d13f23b` on Lean `v4.34.1` — supplies the real analysis, linear algebra and so on, each lemma
itself kernel-checked.

So the first thing I did was read the statement, in `ComparatorChallenges/ThomsonN7.lean`. It is
worth seeing, because a machine-checked proof of the wrong statement is worth nothing:

```lean
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‖⁻¹

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))
```

Three details are load-bearing. `SphereConfig` demands `Function.Injective x` — the points must be
distinct — because in Lean `0⁻¹ = 0`, so without it two coincident charges would contribute zero
energy and the "minimum" would be nonsense. The uniqueness clause quantifies $g$ over all linear
isometries `R3 ≃ₗᵢ[ℝ] R3`, reflections included, and $\sigma$ over all relabellings, which is the
right notion of "the same configuration". And the energy sums over `Finset.Ioi i`, counting each
unordered pair once. Read slowly, this is a faithful encoding of the Thomson problem for seven
points. That it reads correctly is my judgement, not a certified fact — which is the whole weight of
that "not human-certified" line.

What the kernel *does* certify is airtight, and the repo documents it three ways:

- The two theorems depend on exactly **three axioms**: `propext`, `Classical.choice` and
  `Quot.sound`. These are Lean's standard trio — the same ones almost every Mathlib result uses.
  There is no `sorry`, no `native_decide`, no `ofReduceBool`, no added axiom, no `set_option` escape
  hatch. The arithmetic-heavy steps use `decide +kernel`, which runs inside the trusted kernel rather
  than in compiled native code you would also have to trust.
- From a clean clone the full build ran **8,928 jobs** and passed; a Lean "Comparator" confirmed the
  solution proves the fixed challenge statement, and a deliberately flipped statement failed on
  exactly that theorem.
- A **second, independent kernel** — `nanoda`, a Rust re-implementation — re-checked the exported
  proof: **47,854 declarations, no errors**. The same export with a single certificate integer
  changed by one was rejected. Two kernels from different authors agreeing is about as strong as this
  kind of evidence gets.

This is the contrast worth holding onto. [Lanyon](/articles/lanyon-neurosymbolic), which proves PDE
solvers correct, and the skeptic's read of [Leanstral](/articles/leanstral-formal-proofs) both turn
on whether a model quietly used `sorry` or `native_decide` to paper over a gap. Here the axiom list
and the second kernel are the receipts that it did not.

## The shape of the proof

The whole argument hangs on one quantity: $m = \min_{i<j} \langle x_i, x_j \rangle$, the smallest
pairwise inner product, i.e. the most nearly-antipodal pair. The bipyramid has such a pair — its two
poles, at $\langle \cdot,\cdot\rangle = -1$ — so the hard, sharp part of the problem lives where $m$
is close to $-1$. The proof splits on $m$ and handles each slice with its own certificate.

<CaseTree />

If $m \ge -9/10$ (Case 1), there is no near-antipodal pair, and a single three-point semidefinite
bound plus a polynomial minorant proves $E(x) \ge E(P) + 3.2\times10^{-4}$ — a comfortable margin, so
equality never happens here. If $m < -9/10$ (Case 2), the proof relabels so the minimal pair is
$(0,1)$, then covers the interval $[-1, -0.90]$ with **five slabs** and a **cap**:

- Each slab gets its own *typed* three-point certificate and leaves a strict margin,
  $E(x) \ge E(P) + 2.6\times10^{-6}$ — again strict, so no minimiser lives in a slab.
- The cap $[-1, -0.99]$ contains the bipyramid itself, so no strict bound is possible. The best typed
  certificate comes out $2.3\times10^{-16}$ *below* $E(P)$. That near-equality is used as a
  constraint: it forces any competitor into a tube of width $1/165000$ around the bipyramid's Gram
  pattern, a combinatorial argument pins the ring down as a pentagon, and an exact second-order
  analysis finishes — $P$ is a strict local minimum, and the equality case gives uniqueness.

<Figure
  src="https://ai.thesatyajit.com/articles/thomson-n7-lean/fig1.png"
  alt="A horizontal strip of cells over the smallest inner product m. From left: an orange 'cap' cell covering [-1, -0.99]; five green 'slab' cells covering [-0.99] up to [-0.90]; a wide blue 'Case 1' cell for m at least -0.90. Below each group, notes describe its certificate: the cap uses a sharp typed certificate plus rigidity and local minimality; the slabs use one typed three-point certificate each with margin about 2.6e-6; Case 1 uses one untyped three-point certificate plus a degree-10 minorant with margin E(P)+3/10000."
  caption="The case split on the smallest pairwise inner product m. Every cell is closed by exact integer arithmetic checked in the Lean kernel; the cap is the only place where E(P) itself is approached (thomson-n7-lean paper, overview figure)."
/>

The structural point is that only one of the seven cells is hard. Six of them are won with a comfortable
strict margin by pure certificate-checking; all the subtlety — the rigidity argument, the second-order
expansion, the uniqueness — is confined to the cap, the one slice that touches the answer.

## The certificate idea, at a readable level

The engine under all of this is the three-point method of Bachoc and Vallentin, adapted to energy
minimisation by Cohn and Woo. Here is the idea without the machinery.

Fix a configuration. For any triangle of points, with inner products $(u, v, t)$, there is a family
of polynomials $Q_k(u,v,t)$ and, for a real symmetric **positive-semidefinite** matrix $F$, a
guarantee that a certain sum over all triples is nonnegative:

$$\sum_{i,j,l} \big\langle F,\; Y_k(t_{ij}, t_{il}, t_{jl})\big\rangle \ \ge\ 0.$$

This is pure linear algebra — it holds because each term is a sum of two squares. Combine several such
nonnegative sums with a one-variable **minorant** $H(t) \le \varphi(t)$ of the Coulomb kernel
$\varphi(t) = (2-2t)^{-1/2}$, and you can engineer an inequality of the form "energy $\ge$ some
target $e$" that holds for *every* configuration whose inner products stay in a given range. Pick the
PSD matrices and the minorant so that $e \ge E(P)$, and you have bounded the energy from below by the
bipyramid's. The hard part — finding matrices that make the slack a sum of squares — is a
semidefinite program, solved numerically and then rounded.

<Figure
  src="https://ai.thesatyajit.com/articles/thomson-n7-lean/fig3.png"
  alt="Two panels. Left: the Coulomb kernel phi(t) = (2-2t)^(-1/2) as a dark curve and its polynomial minorant H as a dashed orange curve, almost coincident from t = -0.9 up toward t = 1, with H dropping below phi near the right edge. Right: the gap phi(t) minus H(t) on a logarithmic scale, hovering around 1e-5 across the range with green dotted lines marking the bipyramid's Gram values c2, 0 and c1."
  caption="The degree-10 minorant H sits just below the kernel phi on [-0.9, 1). The gap stays near 1e-5 at the bipyramid's own inner products, which is why Case 1's final margin is small but strictly positive (thomson-n7-lean paper, minorant figure)."
/>

Two things make the numerical search irrelevant to correctness, which is the elegant part. First,
**positive-semidefiniteness is checked exactly**: each matrix is stored as pivots, columns and a
diagonally-dominant remainder, so $x^\top F x \ge 0$ reduces to a sum of squares plus an elementary
bound — no floating point. Second, **every polynomial identity is checked by Kronecker substitution**:
evaluate both sides at one carefully chosen big integer and compare, which is sound because the
exponents are spread far enough apart that the evaluation is just a base-$2^w$ expansion of the
coefficients. All the data are integers or rationals over a common denominator like $2^{160}$; the
kernel's built-in big-integer arithmetic does the rest. How the numbers were *found* does not enter
the proof at all — a wrong guess simply fails to check.

The N=7 twist is the word *typed*. Because the bipyramid has two vertex orbits, one symmetric
certificate is not sharp enough near the poles — in the search it left a gap of about $10^{-3}$. So
Case 2 uses two families of PSD matrices, one for a pole root and one for a ring root, and three
separate pair functions $H_A, H_B, H_C$ for the pole–pole, pole–ring and ring–ring classes. The
slack is then distributed across the 35 triples by type. That extra structure is what buys the sharp
bound on the cap.

<Figure
  src="https://ai.thesatyajit.com/articles/thomson-n7-lean/fig2.png"
  alt="Left: the pentagonal bipyramid drawn as a graph. Vertices 0 and 1 are the orange poles at top and bottom; vertices 2 through 6 are the green ring. A dotted line joins the two poles (type A), thin lines join poles to ring (type B), thick solid lines join ring neighbours and dashed lines join ring diagonals (type C). Right: a legend giving the Gram value of each pair type at P — pole-pole t=-1, pole-ring t=0, ring neighbours t=c1, ring diagonals t=c2 — and a note that the 35 triples split as 5 PPR, 20 PRR and 10 RRR, with no pole-pole-pole triple."
  caption="The typed certificate respects the bipyramid's two vertex orbits: poles (type P) and ring (type R). One pair function per class, two root kernels, and three triple types — there is no pole-pole-pole triple because there are only two poles (thomson-n7-lean paper, types figure)."
/>

## How ten agents did it, and the honest part

The process claims are *reported*, not something I can reproduce: ten Claude Sonnet 5.5 agents, about
15 hours, 1,270 messages on a shared board, the certificates found by numerical SDP and rounded to
exact integers. What makes that believable is the structure, not the model. A proof that decomposes
into independent cells, each closed by a self-contained certificate that the kernel verifies in
isolation, is exactly the kind of work that parallelises: every lemma gets a verdict with no human in
the loop, so agents can speculate in parallel up to whatever the checker can confirm. This is the same
observation that made [Jev swarms](/articles/jev-engineering-swarms) interesting — many agents are
useful precisely when the system can verify which work is correct — and the same reason a trusted
kernel matters more than the agent count. Ten agents producing 17,895 lines the kernel accepts is the
part worth sitting with; the kernel is what makes the ten safe.

It is worth putting this next to [Bend 2](/articles/bend-2), which leaned on "proof-checking" as a
marketing line: there the question was whether the checker was real and consistent. Here the checker
is Lean, re-run twice, and the receipts are in `verification/`. The interesting risk has moved.

## What to make of it

The mathematics checks out as far as I can verify it from the repository, and the verification record
is unusually thorough — two kernels, a negative control, an exact statement comparison. But sobriety
is the house position, so here is the ledger.

- **No license.** The repository ships no `LICENSE` file, which legally means all rights reserved. You
  can read it; reusing the Lean code is not clearly granted. (This is why this article does not run any
  of its code — I read it and cloned it, nothing more.)
- **Not peer reviewed, and the only writeup is the blog.** There is a paper in the repo and a
  one-command check, but no journal submission, no arXiv posting, and no first-party account beyond
  the Vals AI [blog post](https://vals.ai/blogs/thomson-n7-lean-proof) and an X thread. The N=8 result
  it builds on is on arXiv; this one is not, yet.
- **"Statement not human-certified."** This is the sharpest caveat, and the repo states it in its own
  description. A machine-checked proof guarantees the *proof* follows from the axioms — it says nothing
  about whether the Lean *statement* faithfully captures the problem. Someone asked exactly this under
  the announcement: "has anyone actually checked the Lean statement matches the problem?" My own read,
  above, says the encoding is faithful, including the injectivity subtlety. But my read is not a
  certification, and a careful independent check of the statement is the one piece of due diligence
  still outstanding.

None of this diminishes what happened: a small open case of a 120-year-old problem now has a proof
that two independent kernels accept, assembled by agents in a day. What it does mean is that the
right claim is narrow and the right posture is to keep reading the statement, not the headline. The
kernel is trustworthy; the framing around it is yours to verify.