Seven Charges on a Sphere: 17,895 Lines of Lean and a 15-Hour Multi-Agent Formal Proof

Place seven like charges on a sphere and let them repel: where do they settle? J.J. Thomson asked this in 1904 while modeling the atom. The plum-pudding model was overturned by experiment, but the geometry problem survived for over a century.

Until now, the N=7 answer was numerical only: a pentagonal bipyramid, five points around the equator and one at each pole. Computing a minimum is one thing; proving all other configurations have higher energy is quite another.

In September 2026, Vals AI released a formal proof. Ten Claude Sonnet 5.5 agents ran for about 15 hours, producing a 17,895-line Solution.lean importing only Mathlib, establishing the pentagonal bipyramid as the unique minimizer for N=7 (rotations and mirrors excluded).

🧲 Seven points, a continuous infinity of rivals

The Thomson energy is the sum of \(1/\|x_i-x_j\|\) over all pairs. Proving a candidate beats every rival means beating a continuous infinity of configurations—no finite search can cover it.

N=7 adds a wrinkle: the pentagonal bipyramid has two inequivalent point classes (poles and equatorial vertices), so certificates and Lean types must treat both roles separately; the N=8 machinery doesn't transfer. For scale: the N=8 rigorous proof (Kryvonos, Liehr, Taylor, arXiv:2609.22077) came less than a month earlier, followed by Lean development by Tooby-Smith and Zughaid.

📐 One scalar, three regimes

The proof partitions configurations by the minimum pairwise inner product m (m near −1 means a nearly antipodal pair):

| m range | Method | Margin over E(P) | |---|---|---| | m ≥ −0.90 | SDP certificate, degree-5, 3-point, based on Bachoc-Vallentin and Cohn-Woo energy forms | at least 3×10⁻⁴ higher | | −0.99 ≤ m ≤ −0.90 | five slabs excluded individually, each with a 3-point certificate | ~2.6×10⁻⁶ higher per slab | | m ≤ −0.99 | near-antipodal certificate + interval arithmetic, then exact second-order local analysis | preliminary bound dips 2.3×10⁻¹⁶ below E(P) |

🔢 Why one matrix can govern infinitely many points

The SDP certificate derives a universal energy inequality from a positive semidefinite polynomial matrix—one inequality valid for *any* configuration on the sphere, taming the infinity at once. A numerical solver finds coefficients, which are then rounded to exact integers/rationals and checked arithmetically by Lean.

The division of labor is key: the solver is a *generator* of certificates, not in the trust base. If it errs, its exact output fails Lean compilation.

The final cap couldn't rely on SDP bounds alone (the margin fell slightly short), so interval arithmetic strictly confines remaining configurations near the bipyramid, and second-order computation proves strict local minimality and characterizes equality.

🔍 Five checks, narrowing the trust base

The artifact is a single Solution.lean. Vals lists five verification steps:

1. Clean build (~10 minutes) 2. Comparator checks against two fixed propositions 3. Axiom audit: only propext, Classical.choice, Quot.sound 4. Independent kernel nanoda accepts 47,854 declarations 5. Mutation testing: changing one integer gets the proof rejected

Two kernels agreeing reduces the exposure of any single checker being buggy. The mutation test verifies not that the proof is correct, but that the checker rejects wrong proofs.

🤖 1,270 messages in 15 hours

Setup: ten Sonnet 5.5 agents sharing one Lean project, with a message board and maximum-effort mode. The initial brief offered nine directions agents could abandon, merge, or contest. Agents exchanged 1,270 messages over 15 hours.

One agent acted as integrator, inlining verified contributions into Solution.lean. A candidate had to pass three gates to enter the final artifact: reproducible build, comparison against fixed theorem signatures, and axiom audit.

Opinion: this arrangement is more interesting than "ten agents writing separately." Parallel exploration converges not by voting, but by having exactly one process hold the final dependency graph.

🧱 Four transferable practices

• Pin down theorem signatures first: once the machine-checkable goal is fixed, success criteria don't drift.
• Separate search from trust: numerical tools may propose candidate certificates; exactness belongs to the proof assistant.
• Integration needs clear ownership: parallel exploration only works when one process holds the final dependency graph and build.
• Test your verifier: clean builds, axiom audits, independent kernels, and deliberate mutations catch different failure modes.

The repo also includes a line-by-line correspondence table between the mathematical argument and the formal implementation—the most labor-intensive and easily overlooked part of the artifact.

⚠️ Limitations

Kernel acceptance only guarantees the formal conclusion follows from the two fixed propositions and their dependencies; whether those propositions faithfully encode the Thomson problem itself requires separate human review—a gap common to all formal methods.

Mutation testing changed only one integer, with no systematic mutation set. Process metrics (15 hours, 1,270 messages) are self-reported by Vals with no third-party replication reported.

Sources: Vals AI blog vals.ai/blogs/thomson-n7-lean-proof and repo github.com/huwngtran/thomson-n7-lean; N=8 paper arXiv:2609.22077.