A Lean Proof of the Thomson Problem for Seven Electrons

The Thomson problem asks how a given number of electric charges arrange themselves on a sphere when each pushes the others away, settling where the total repulsion energy is lowest. For seven charges, numerical searches have pointed to the same answer for decades: a pentagonal bipyramid, with five points around the equator and one at each pole. Proving it is harder, because a proof has to rule out every other arrangement and those arrangements form a continuous space. According to the post, rigorous answers exist for only a few small cases; five charges needed a computer-assisted proof, and a proof for eight was posted on 18 September 2026.

Hung Tran of Vals gave ten Claude Sonnet 5.5 agents from Anthropic a shared message board, a project in Lean, a proof assistant whose small trusted core, the kernel, checks every step, and two fixed statements to prove. One says the bipyramid has the lowest energy; the other says every lowest-energy arrangement is that same shape, rotated, reflected or relabeled. After about 15 hours and 1,270 messages, they had a proof of both. The brief suggested nine directions, including adapting the eight-charge work, and one agent took on the job of assembling the verified pieces into a single file.

The proof sorts every arrangement by how close its most widely separated pair of points comes to being exactly opposite, then rules out each range with a certificate, a set of numbers that proves an energy bound. The certificates were found with a numerical optimizer and rounded to exact values, and Lean checks those exact values, so the result does not depend on the solver or on floating-point arithmetic. The method builds on the eight-charge results by Kryvonos, Liehr and Taylor, published on arXiv, and on a separate Lean development by Joseph Tooby-Smith and Alex Zughaid.

The trust case rests on checks rather than on the agents. The 17,895-line file builds from a clean copy and uses only Lean's standard axioms. A comparison tool confirmed it proves exactly the fixed statements, and a second, independently written kernel accepted it, while changing a single integer in the certificate data made that kernel reject it. These checks are the author's own, but the sources, scripts and logs are on GitHub for others to rerun.