The Thomson problem: where do electrons settle on a sphere?

Take seven electrons and confine them to the surface of a ball. Every pair of them repels, and none of them can leave the surface, so they spread out until no small move lowers their energy. Where do they end up?

With two electrons the answer is obvious: they sit at opposite poles. Three form an equilateral triangle on a great circle, and four sit at the corners of a regular tetrahedron. For seven, computer experiments have long agreed on one picture: an electron at each pole and five around the equator, at the corners of a regular pentagon. Proving that no other arrangement does better was another matter. A complete proof appeared only in September 2026, and most of it was written by ten AI agents in about fifteen hours.

What is the Thomson problem?

Place N points on a sphere of radius 1 and treat them as equal electric charges. Each pair contributes the reciprocal of its distance to the total energy:

Here x₁, …, x_N are the positions of the points, and the sum runs over all pairs. The Thomson problem asks for the arrangement with the smallest possible energy. Two points that come close add a lot to the sum, so a good arrangement spreads the points out. On a sphere, though, “spread them out evenly” is not a precise instruction, and for most values of N it does not point to one obvious pattern.

The problem is named after J. J. Thomson, who discovered the electron in 1897. In 1904 he proposed a model of the atom in which electrons are embedded in a ball of positive charge, later nicknamed the plum pudding model, and he studied how the electrons would arrange themselves. Rutherford’s nucleus replaced that model a few years later. The mathematical question stayed.

Which arrangements were known to be best?

For some values of N the answer has been settled for decades. Two points sit at opposite poles. Three form an equilateral triangle on a great circle. Four, six and twelve points sit at the vertices of a regular tetrahedron, octahedron and icosahedron. In 2007 Henry Cohn and Abhinav Kumar showed that these five arrangements are optimal in a much stronger sense: they minimize not only the Coulomb energy but every energy from a broad class of repulsive interactions. They are called universally optimal.

Five points show how delicate the problem can be. The winner for the Coulomb energy is the triangular bipyramid, with one point at each pole and three on the equator. Richard Schwartz proved this in 2010 with a computer-assisted argument, published in 2013. The bipyramid is not universally optimal. If the repulsion is replaced by one that falls off much faster with distance, like 1/r^s with s above about 15, a pyramid with a square base does better.

Why is the cube the wrong answer for eight?

Eight is where intuition fails. The cube looks like the natural way to spread eight points over a sphere: all its vertices lie on one sphere, and they all look alike. Yet the cube does not minimize the energy. Turn one of its square faces by 45 degrees, so that its corners no longer sit directly above the corners of the opposite face, and the energy drops from 19.7408 to 19.6816. Move the two squares slightly toward each other and it falls further, to 19.6753. The result is a square antiprism.

Square faces are a sign of wasted space: the center of a square is far from all four of its corners. The antiprism keeps two squares and turns the other four into eight triangles.

The square antiprism had been the expected answer for decades. A proof appeared in September 2026. Liudmyla Kryvonos, Lukas Liehr and Mitchell A. Taylor showed that, up to rotations and reflections, it is the only arrangement of eight points with the lowest energy, both for the Coulomb energy and for the logarithmic energy. Their proof is computer-assisted and fully verified in Lean, a programming language in which a computer checks every step of a proof.

The paper also says how the proof was found. In a section on the use of large language models, the authors write that “the main ideas in the proofs of Theorems 1.1, 1.2 and 1.3 are due to GPT-6 Astra”. Their own part included understanding the proof, simplifying the numerical work and verifying the numerical certificates in Lean.

How do you prove that nothing does better?

Finding a good arrangement is the easy half. A computer can scatter N points at random, let them repel each other, and repeat the experiment thousands of times. For small N almost every run ends in the same place. Such experiments are convincing, but they prove nothing: there are infinitely many arrangements, and a search can never visit them all.

Searches can also get stuck. Besides the best arrangement there are others in which no small move lowers the energy, and their number grows quickly with N. One study estimated that for N close to 200 there are at least tens of thousands of them.

A proof has to deal with every arrangement at once. The main tool is a lower bound: an inequality showing that, wherever the points are, the energy cannot fall below a certain number. If that number equals the energy of the candidate, the candidate has won. The classic way to get such a bound is to replace the energy of a pair by a carefully chosen polynomial that never exceeds it. Sums of such polynomials over all pairs of points on a sphere can be bounded from below without knowing where the points are. For two, three, four, six and twelve points the bound is exact, and that is how Cohn and Kumar handled them.

For seven and eight points this bound falls short. The 2026 proofs add bounds that look at triples of points instead of pairs, computed by semidefinite programming, and where necessary they split the possible arrangements into cases. Near the candidate, a separate argument shows that every small change raises the energy, so the candidate is the only winner. In the end everything comes down to a long list of numerical inequalities, and every one of them has to be checked exactly, not approximately.

Computers are good at this part, and Lean makes their work trustworthy. A proof written in Lean is accepted only if a small program, the kernel, can check every step from the definitions. What Lean cannot check is whether the theorem says what we think it says. People still have to do that.

What exactly did AI do?

Ten days after the eight-point paper, on 28 September 2026, Hung Tran of Vals AI described a Lean proof for seven points. He wrote the two statements to be proved himself: that the pentagonal bipyramid has the lowest energy, and that up to rotations and reflections it is the only arrangement that does. He then set ten Claude Sonnet 5.5 agents to work, with a shared message board and a brief that proposed nine possible directions. After about fifteen hours and 1,270 messages the agents had produced a single file of 17,895 lines. It was checked by Lean and, independently, by a second proof checker called nanoda.

The agents did not invent the method. Their brief pointed them to the eight-point work, and the lower bounds they used come from it. What they did was the long, careful job of adapting those techniques to a new case and getting every inequality past the checker. The repository that accompanies the proof carries a plain warning: “Statement not human-certified. Not peer reviewed.”

On 6 October a similar project appeared for nine points. Its winner is the tricapped trigonal prism: a triangular prism with an extra point above each of its three side faces. According to its README, the proof is “AI-generated by Claude Opus 5.5 and Codex”. Aravind Karthigeyan, who directed and published the project, does not claim to have written it, and the repository asks for external review.

On 22 October, while this article was being written, a Lean proof for ten points was posted to a public GitHub repository of proposed solutions to open problems. It adapts the nine-point project and identifies the winner as the bicapped square antiprism: the eight-point antiprism with an extra point at each pole. The repository describes the result in one line: “Checked in Lean from the definitions; not yet reviewed by experts.”

Which cases of the Thomson problem are solved?

This is the state of the problem on 23 October 2026. Energies are rounded to nine decimal places.

So has AI solved the Thomson problem?

No. Each of these proofs settles a single value of N, and the Thomson problem asks about all of them. As of 23 October 2026, eleven points and every N from thirteen on remain open: no proof has been announced for any of them.

The cases also get harder. The calculations grow, and the best arrangements lose their symmetry: the best known arrangement of eleven electrons is much less regular than those for nine or ten. For every unsolved N, the best arrangements we know come from computer searches. For large N there is no guarantee that a search has found the best one, and no one expects a formula that gives the answer for every N.

Some features of the best arrangements, however, can be predicted exactly. This is where a soccer ball comes in.

What do electrons have in common with a soccer ball?

Give each electron the part of the sphere that is closer to it than to any other electron. These regions, called Voronoi cells, divide the sphere into polygons, and in a typical arrangement three cells meet at every corner. A cell with k sides belongs to an electron with k nearest neighbors.

In a large flat crystal every particle has six neighbors and every cell is a hexagon. A sphere does not allow that. If all the cells are pentagons, hexagons and heptagons, the count that explains the twelve pentagons on a soccer ball gives

For 32 electrons, the best known arrangement has twelve pentagonal cells and twenty hexagonal ones: the pattern of a classic soccer ball. For 400 electrons, computer searches find arrangements with extra defects. The one below has 19 pentagons and 7 heptagons, and again 19 − 7 = 12.

Euler’s formula fixes this balance. It does not say where the defects should go, or which of the many arrangements allowed by topology has the lowest energy. That is the hard part of the Thomson problem.

In larger systems the extra defects line up in short chains of alternating pentagons and heptagons, called scars. They have been seen in experiments. In 2003 a team of physicists imaged plastic beads about a micrometer across, packed on the surface of water droplets in oil. Above a critical size, around 360 beads on a droplet, scars appeared.

Common questions

Sources and further reading: Kryvonos, Liehr and Taylor, Energy minimization for eight points on the sphere (arXiv, 2026); Hung Tran, A Lean Proof of the Thomson Problem for Seven Electrons (Vals AI, 2026) and its repository; the nine-point Lean project (Zenodo archive); the ten-point Lean project; Cohn and Kumar, Universally optimal distribution of points on spheres (2007); Schwartz, The 5 electron case of Thomson’s problem (2013); Calef, Griffiths and Schulz (2015), on the number of stable arrangements; Bausch et al., Grain boundary scars and spherical crystallography (2003); and the table of energies on Wikipedia.