Ten Claude agents generate a verified proof for Thomson N=7

Vals AI reports that ten Claude Sonnet 5.5 agents produced a formal proof of the seven-electron Thomson problem in about 15 hours. The resulting Solution.lean file spans 17,895 lines, satisfies two fixed challenge statements, and establishes the pentagonal bipyramid as the unique minimum up to rotation, reflection, and relabeling.

Lean accepted the proof, and an independent kernel implementation checked the generated declarations. The experiment combines numerical optimization, exact certificates, interval arithmetic, and agent coordination to address a problem whose seven-point case had resisted a rigorous global proof for more than a century.

Seven charges leave an infinite search

The Thomson problem asks how N identical charges arrange themselves on a sphere to minimize Coulomb energy. For unit vectors x₁, …, x_N, the energy is the sum of 1 / ‖xᵢ − xⱼ‖ over every pair. A global proof must compare one candidate with a continuous, infinite family of configurations.

For N = 7, numerical calculations have long selected a pentagonal bipyramid, with five points around the equator and one at each pole. The formal challenge is to prove that every other configuration has higher energy and to classify every equality case.

One scalar divides the proof

The proof partitions all configurations using m, the smallest pairwise inner product. Since the distance between two unit vectors is determined by their inner product, a value near −1 identifies an almost antipodal pair. That distinction leads to separate global bounds.

A semidefinite-programming certificate derives a universal energy inequality from a positive-semidefinite matrix of polynomial data. Numerical solvers searched for suitable coefficients, which were then rounded into exact integer or rational data. Lean checks the resulting arithmetic, so the numerical solver serves as a certificate generator rather than part of the trusted proof.

The final cap requires more than the semidefinite bound because its margin falls slightly below the target energy. Interval arithmetic rigorously confines the remaining configurations near the pentagonal bipyramid, while the second-order calculation proves strict local minimality and identifies the equality cases.

Five checks narrow the trust base

The released artifact is a single Solution.lean file that imports only Mathlib. Vals reports five verification steps:

1. Clean build: The file compiles from a fresh copy in about ten minutes.
2. Statement comparison: A Comparator checks the result against the two fixed challenge statements.
3. Axiom audit: #print axioms reports only propext, Classical.choice, and Quot.sound.
4. Independent kernel: Nanoda accepted 47,854 declarations without errors.
5. Mutation test: Changing one integer in the first case caused the independent checker to reject the proof.

Agreement between Lean and Nanoda reduces exposure to a defect in either checker, while the axiom report makes the logical assumptions explicit. Reviewers must separately confirm that the fixed Lean statements faithfully encode the intended Thomson problem; kernel acceptance establishes that the formal conclusions follow from those statements and dependencies.

Earlier machinery meets new geometry

The construction builds on the computer-assisted proof for N = 8 by Kryvonos, Liehr, and Taylor, described in the N=8 paper, along with the Lean development by Joseph Tooby-Smith and Alex Zughaid.

The seven-point geometry requires a distinct formal treatment because the pentagonal bipyramid has two inequivalent classes of points: poles and equatorial vertices. The proof therefore uses separate certificate families and Lean types that preserve those roles throughout the argument.

Ten agents converge on one file

The experiment gave ten Claude Sonnet 5.5 agents a shared Lean project, a message board, and a maximum-effort configuration. During the 15-hour run, they exchanged 1,270 messages. The initial brief proposed nine directions, and the agents could abandon, combine, or challenge them as the proof developed.

One agent assumed the integrator role and inlined verified contributions into Solution.lean. A candidate entered the final artifact only after a reproducible build, comparison with the fixed theorem signatures, and an axiom audit.

A workflow developers can reuse

The run exposes four engineering practices for agent-assisted formal verification:

• Fix theorem signatures first. Stable machine-checkable targets prevent the success criterion from drifting during exploration.
• Separate search from trust. Numerical tools can propose certificates while the proof assistant checks exact data.
• Assign integration ownership. Parallel exploration becomes useful only when one process controls the final dependency graph and build.
• Test the verifier. Clean builds, axiom audits, independent kernels, and deliberate mutations catch different failure modes.

The GitHub repository contains the paper, Lean source, checking scripts, and a line-by-line map between the mathematical argument and its formal implementation. Together, those artifacts provide a reproducible example of numerical certificate search, exact formal checking, and multi-agent proof integration.