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

2026-10-02 · 14 min · formal-methods · theorem-proving · agents · verification · llm · explainer

A 1:33 narrated explainer, drawn in code. Every number and picture in it is this article's own; the sources are below.

› transcript

Hi, I'm Marlo! Seven charges on a sphere settle into a pentagonal bipyramid, and ten agents wrote a proof of it. The idea: slice the problem by the closest pair of points, and give each slice a certificate the kernel checks exactly. Take any seven distinct points, and find the two that are closest to opposite. If no pair is nearly opposite, one bound settles the whole case. If a pair is nearly opposite, cover that region with five slabs and a cap. Each slice gets a certificate built from positive matrices and a lower bound on the energy. The Lean kernel checks every certificate as exact integer arithmetic. The energy is just a sum of inverse distances. Each pair adds one over the distance between the two points. Sum that over all twenty-one pairs of points. On the left, a cap and five slabs cover the nearly-opposite region. On the right, a single case covers everything else, with room to spare. The answer's energy is fourteen point four five, and every certificate has to beat it. A second, independent kernel re-checked all forty-seven thousand declarations, with no errors. Six slices fall to a certificate; only the slice holding the bipyramid needs the hard argument. To recap: split on the closest pair, bound each slice, and let two kernels check the whole thing. Every source is in the full article. I'm Marlo. Bye!

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. 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, 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.

Coulomb energy

14.9953

minimum E(P) = 14.4529774142

startpentagonal bipyramid

Illustrative, not a solver: the seven points are blended from a fixed suboptimal start toward the exact bipyramid and reprojected onto the sphere, so the energy falls to 14.4529774142. The proof is about why that configuration is the global minimum, not how a descent finds it.

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 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:

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, which proves PDE solvers correct, and the skeptic's read of Leanstral 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.

split on m = min inner product → one certificate per cell

cap[-1, -0.99]

certificate: typed 3-point, then rigidity + local minimality
margin: E(P) - 2.3e-16 (near-sharp)

Contains the bipyramid itself, so the certificate cannot be strict here — it comes 2.3e-16 below E(P). That near-equality confines any rival to a tube of width 1/165000 around P's Gram pattern; a combinatorial argument forces the ring into a pentagon, and an exact second-order expansion proves P is a strict local minimum. This is the only cell that yields the uniqueness clause.

Seven cells, closed left to right by exact integer arithmetic in the Lean kernel. The five slabs and Case 1 leave a strict gap above E(P); only the cap, which contains the bipyramid, is handled by rigidity and an exact local-minimality argument, and it is the cell that proves uniqueness.

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.

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. — 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.

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. — 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.

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. — 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 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, 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 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.