Ten AI agents deliver a computer-checked proof for a puzzle with seven electrons in fifteen hours

Put a few electrons on a sphere. They push each other away and keep moving until the total energy is as low as possible. What shape do they end up in? The British physicist J.J. Thomson asked this question in 1904, when he was trying to understand how electrons sit in an atom. Since then it has been called the Thomson problem.

For seven electrons, researchers have known the answer for decades from computer calculations: five electrons in a ring around the equator and one at each pole. Together they form a double pyramid with a pentagon as its base. But a calculation that keeps finding the same shape is not yet a proof. There are infinitely many ways to put seven points on a sphere, and a proof has to show that none of them has less energy. Such a proof existed only for a few numbers: 2, 3, 4, 6 and 12 electrons, for 5 electrons since 2013 with the help of a computer, and for 8 electrons since September 2026.

Ten agents, one proof

At the end of September, Hung Tran of Vals AI, a company that tests and compares AI models, reported that it has now also been done for seven electrons. Tran put ten AI agents to work: AI programs that carry out tasks on their own, in this case all using the model Claude Sonnet 5.5 from Anthropic. They were given the exact task, a shared noticeboard to discuss things and nine possible approaches. One of them was to adopt the method that had worked for eight electrons shortly before. The agents were free to choose which approaches to pursue, combine or drop.

After about fifteen hours and 1,270 messages, there was a proof. One agent took on the job of putting everything together without being asked, and merged all the approved pieces into a single file of 17,895 lines. The proof says two things: no arrangement of seven electrons has less energy than the double pyramid, and every arrangement with exactly that energy is the same double pyramid, only rotated or mirrored.

A computer checks every step

The proof is written in Lean, a programming language for mathematics. Every step is written down so precisely that software can check whether it is correct. This means nobody has to take the AI's word for it. According to Tran, Lean accepted the proof, and a second, separately built checking program also found no errors. As a test, Tran changed one number in the proof, after which that second program rejected it at once. The proof is publicly available on GitHub, so anyone can repeat the check themselves.

How the proof works

Trying out all the infinitely many arrangements is impossible. That is why the proof works with a lower bound: a number below which the energy can never fall. If that lower bound matches the energy of the double pyramid exactly, no other arrangement can be better.

For seven electrons, this cannot be done in one go. So the proof divides all possible arrangements into groups. It looks at the pair of electrons that is closest to lying exactly opposite each other, because in the double pyramid the two poles lie exactly opposite each other. If no two electrons lie almost opposite each other, the energy always stays clearly above that of the pyramid. The arrangements in which they do are checked in smaller pieces. What remains are arrangements that are almost the same as the pyramid itself. A final, very precise calculation shows that the pyramid is the lowest point there.

The numbers for all those bounds were first found by a calculation program. Such a program works with rounded decimal numbers and therefore makes small errors. That is why the numbers were then converted into exact fractions, which Lean recalculates itself. So the proof does not depend on the program that found the numbers.

What still needs to happen

Tran points out that mathematicians have not yet reviewed the proof and that it has not appeared in a scientific journal. Lean shows that the proof is correct for the task as it was written down in Lean. Experts can now check whether that task describes the Thomson problem exactly. Vals AI did the checks itself; because everything is public, others can repeat them.

Jason Rute, who works on mathematics that computers can check, called the result impressive. According to Rute, the earlier proof for five electrons was a separate computer calculation, and it was not even clear whether it could be put into Lean. The new result applies to seven electrons; each number of electrons is a separate puzzle.

On to ten, nine and thirty-two

On 27 October, Vals researcher Jacob Stavrianos explained how the proof works and which numbers could come next. According to the company's calculations, the same approach should work first for ten and then for nine electrons. For 32 electrons, which are expected to be arranged like the panels of a classic football, the method falls short according to Vals AI, and a new idea is needed. The tasks for 9, 10 and 32 electrons are on the website Prove2Me, where anyone can submit a proof.

Teams of AI agents working with Lean are now showing results in more places. At Axiom Math, dozens of agents converted an existing proof of some 15,000 pages into code that a computer checks. That was a proof humans had already written. At Vals AI, the agents came up with a proof themselves for a case for which no proof existed yet.

What does this mean for the road to the singularity?

Ten AI agents divided the work among themselves, discussed it, dropped approaches that led nowhere and combined the pieces into one proof for an open mathematical question. That is more than giving an answer: it is doing research independently, in a few hours instead of years. And because a computer checks every step, nobody has to trust the AI blindly. That combination makes it possible to give AI ever larger research questions. The next test is whether the same approach can also handle ten and nine electrons, and who finds the new idea for 32.

What is the technological singularity? Read the explanation →