Ten Claude Sonnet 5.5 agents have produced a formal proof for the N=7 case of the Thomson problem, a 122-year-old question in mathematical physics.
According to MarsBit, citing the WeChat account Xinzhiyuan, the agents worked for 15 hours, exchanged 1,270 technical messages, and wrote 17,895 lines of Lean code. The result was a proof that the pentagonal bipyramid is the minimum-energy configuration for seven electrons constrained to a sphere.
A century-old gap in the Thomson problem
The report traces the problem back to 1904, when J.J. Thomson, the discoverer of the electron, introduced the "plum pudding" model and studied how electrons might arrange inside an atom. That atomic model was later overturned by Rutherford, but the mathematical question survived as the Thomson problem.
Its statement is simple: place N electrons on the surface of a sphere, let them repel each other, and ask which arrangement minimizes total energy. The difficulty is global. Pulling one pair farther apart can force other points closer together, so numerical intuition is not enough.
Over the past 122 years, only a small number of cases had been settled rigorously. The cases N=2, 3, 4, 6, and 12 were handled through geometric symmetry. The N=5 case was not proved until 2013, when mathematician Richard Schwartz completed it with computer assistance. For N=8, the report says Kryvonos, Liehr, and Taylor posted a proof on arXiv on Sept. 18 this year and formalized it in Lean.
N=7 had remained open in between. Numerical simulations over many years repeatedly pointed to the same elegant arrangement, the pentagonal bipyramid: five electrons evenly spaced around the equator, with one fixed at each pole. Its theoretical energy is about 14.4529774142. But simulation is not proof, and without a complete logical closure, the possibility of some obscure lower-energy "ghost configuration" could not be eliminated.
How the 10-agent experiment was set up
The task was assigned by Hung Tran of Vals AI to what the report describes as a virtual laboratory made up of 10 Claude agents.
Humans fixed the boundary conditions at the start. The 10 Claude Sonnet 5.5 agents were placed in an interactive board and a Lean proof environment, all set to maximum compute effort, with a single target: prove that the pentagonal bipyramid is the minimum-energy arrangement for seven electrons on a sphere.
No step-by-step method was supplied. The agents were given only two fixed Lean theorem statements and nine possible exploration directions. From there, the next 15 hours were left entirely to the agents.
During that period, they exchanged 1,270 technical messages. Some tried an approach, found it failed, and posted the dead end. Others revised those attempts. At least one agent noticed that separate lines of work could be merged. Later, one Claude took on the role of integrator and assembled verified components into a single file named Solution.lean.
The hard rule was straightforward: if it did not pass the checker, it did not count. The proof had to compile from scratch, match the exact problem statement, and avoid introducing extra axioms. The final product ran to 17,895 lines of Lean code.
The proof strategy
The core method, as described in the report, was to partition the continuous configuration space by the minimum inner product m between any two electrons, then handle each region separately.
Region one: m ≥ -0.90
In this region, no pair of electrons lies close to antipodal points. The agents used a fifth-degree three-point semidefinite programming bound together with exact integer data that could be checked directly by the kernel. That established that every configuration in this region has energy at least 3×10⁻⁴ above the pentagonal bipyramid.
Region two: m < -0.90
This part was more difficult because it includes pairs that are close to antipodal. The agents split it again.
- For the five slices in [-0.99, -0.90], each slice was ruled out with a strict three-point certificate, giving an energy lower bound about 2.6×10⁻⁶ above the optimum.
- For the polar-cap region m ≤ -0.99, the proof used a high-precision certificate. That certificate produced an energy lower bound only 2.3×10⁻¹⁶ below the energy of the pentagonal bipyramid.
The report describes this as an extremely narrow window. It compressed all possible challengers into a tiny neighborhood around the pentagonal bipyramid. From there, Claude used interval-arithmetic rigidity arguments and an exact second-order local minimality theorem to lock down uniqueness.
One key step came at the end: all numerical certificates were rounded and converted into exact integers and rational numbers. That removed floating-point error and cut out any dependence on external solvers, leaving the proof grounded in exact algebraic operations.
Two layers of verification
The article gives specific verification data.
- Lean’s kernel completed a full compilation in 599 seconds. Within that run, lake build took 344 seconds and finished 8,928 compilation tasks.
- The independent kernel nanoda checked 47,854 declarations and found zero errors.
- In a negative-control test, changing just one integer in the proof data caused nanoda to stop with an error immediately.
That last detail is central to the report’s credibility claim: a one-integer change was enough to break verification, which shows how tightly the proof data and the formal structure are linked.
From problem solving to research work
The article places the experiment in a broader shift in mathematical AI. In the past, saying AI could do math often meant it could solve a given problem and return an answer. Here, the agents handled a longer research chain: exploring proof routes, running parallel trial and error, deciding which directions were worth pursuing, merging code into one file, and submitting the result to machine verification.
According to the source text, there was no human intervention in the proof process and no preset division of labor. The 10 Claude agents organized discussions on their own, divided work on their own, merged code on their own, and completed validation on their own.
The article closes by arguing that what happened over one night was not only the proof of a long-open conjecture, but also a demonstration that AI is ready to work with humans on mathematics.
The original piece was published on the WeChat account Xinzhiyuan and credited to ASI Qishilu. MarsBit republished the report.