AI Didn’t Solve the Thomson Problem. It Built a Proof Factory.

On September 30, 2026, Xinzhiyuan published an article. The headline said ten Claude 5.5 models had cracked a century-old physics conjecture. The article listed numbers: 15 hours, 1,270 messages, 17,895 lines of Lean code. Then it said AI had begun doing research on its own.

Those numbers are real. The judgment that it was “doing research on its own” omits several key qualifiers.

I. Why N=7 is hard

In 1904, J.J. Thomson proposed the plum pudding model. Rutherford later overturned the model, but the mathematical problem survived: place N mutually repelling electrons on a sphere. How should they be arranged so total repulsive energy is lowest?

This is the Thomson problem.

For N=2, two points sit at opposite poles. For N=3, an equilateral triangle. For N=4, a regular tetrahedron. For N=6, a regular octahedron. For N=12, a regular icosahedron. Geometric symmetry solved these. N=5 waited until 2013, when mathematician Richard Schwartz completed a proof with computer help. N=8 was posted to arXiv on September 18, 2026, by Kryvonos, Liehr, and Taylor, and formalized in Lean.

N=7 sat in the middle, blank for 122 years.

For decades, supercomputers ran numerical simulations. The results pointed to the same configuration: a pentagonal bipyramid. Five electrons evenly spaced around the equator, one pinned at each pole. The theoretical energy value is about 14.4529774142.

Almost everyone believed the simulation result. Believing is not proving. The Thomson problem asks for a global optimum: the arrangement with the lowest total energy among all possible arrangements. A locally stable arrangement is not enough. To rule out countless local minima, symmetry breaking, and combinatorial explosion, you need a rigorous proof.

That is the difficulty of N=7.

II. What the Vals AI experiment actually did

Vals AI had 10 Claude Sonnet 5.5 agents collaborate. They worked through the night for 15 hours, exchanged 1,270 messages, and wrote 17,895 lines of Lean code. The proof passed double verification by the Lean kernel and the independent kernel nanoda. nanoda accepted 47,854 declarations with no errors. Change one integer, and nanoda reports an error.

The promotional language said: “No human intervention, no preset division of labor. Ten Claude 5.5 models formed their own group, argued among themselves, chose their own algorithms, and merged their own code.”

Those descriptions may hold at the technical level. At the semantic level, they omit preconditions.

Before the 10 Claudes began, humans had already done several things. They provided two already-written Lean theorem statements, which set clear proof targets. They gave nine suggested directions, including “port over the N=8 method,” LP bound, splitting by combinatorial type, and verified certificate engine. Ten days earlier, the complete computer-assisted proof for N=8 had been made public, also verified in Lean. That work established core proof tools such as linear programming and three-point semidefinite programming.

After N=8 had been run through, Vals AI put N=7 in and let 10 Claudes work inside the target, tools, and strategy space given by humans. The agents ground out a complete proof.

There was no real-time human intervention. There was human upfront design.

There was no preset division of labor. The goal, constraints, available tools, and success criteria were all preset.

III. Mathematical discovery vs. proof engineering

Mathematical discovery includes posing new problems, inventing new methods, finding new conjectures, and breaking through core difficulties.

Mathematical proof engineering includes exhaustively enumerating cases under a known strategy, combining lemmas, generating code, verifying boundaries, merging modules, and ensuring formalization passes.

This time, the AI did the latter.

It did not invent three-point semidefinite programming. It did not propose the LP bound. It did not discover the pentagonal bipyramid. It did not solve the core mathematical difficulty of adapting the N=8 method to N=7. That difficulty had very likely already been overcome in the human work of September 18.

What it did was start the machine tools on blueprints drawn by humans. It manufactured a proof that met specifications, at high speed, in parallel, and reliably.

“No human intervention” means no real-time human intervention. Before the task began, humans intervened. The theorem statements were written by humans. The exploration directions were given by humans. The core tools had just been built by humans. The problem boundary was locked down by humans.

“No preset division of labor” means no one specified which Claude was responsible for which part. The goal, constraints, available tools, and success criteria of the entire task were preset.

A more accurate statement: within a formalized target and strategy space preset by humans, the AI used multi-agent collaboration to complete the engineering implementation and verification of a research-grade mathematical proof.

IV. The automated pipeline

The breakthrough is here. An automated pipeline for research-grade mathematical search and formalization engineering has taken shape.

The input end is a clear formalized problem statement, plus a set of already-verified proof strategies and a tool library.

The output end is machine-verifiable, logically error-free proof code.

When those two conditions are met, AI can run the process with extreme efficiency.

A human team may take months to years to complete and formalize the computer-assisted proof for N=8. AI compressed the generation of the N=7 proof into 15 hours. That cuts the work from months or years to 15 hours. That is an order-of-magnitude gain.

Reliability comes from formal verification. The proof passed double verification by the Lean kernel and the independent kernel nanoda. nanoda accepted 47,854 declarations with no errors. As long as humans trust the formal verification tools, they can trust the logical correctness of this proof without checking 17,895 lines of code line by line.

This provides a working solution to the credibility problem for AI-generated mathematical proofs. Do not trust the AI’s intuition. Trust the logical determinacy of the formal kernel.

V. The chain of trust and publication

One sentence in your original text is precise: “Now, as long as the direction is supported and there is a certain foundation, research-grade mathematical search and formalization engineering can be strung together through AI into an automated pipeline. So the question is whether you dare to believe it. If AI grinds out a Lean proof for you, as long as you dare to believe it, you dare to publish it.”

That hits the center.

In the future, mathematical papers may no longer rely on human reviewers checking proofs line by line. They may rely on formal kernels such as Lean and nanoda. Reviewers only need to check a few things. Is the theorem statement faithful to the original problem? Is the proof strategy reasonable? Has the AI-generated code passed kernel verification?

If all those are satisfied, an AI-generated Lean proof can be published. We are not being asked whether AI understands mathematics. We are being asked whether formal verification is enough for mathematical truth.

Behind this is a chain of trust. Trust the logical correctness of the formal tools. Trust that the theorem statement is faithful to the problem humans want to solve. Trust that the human-given strategy direction has not led AI toward a wrong target. Trust that the AI-generated code has not substituted concepts during formalization. Trust that the entire collaboration process contains no hidden human intervention or data contamination.

As long as this chain of trust holds, a Lean proof ground out by AI can become mathematical knowledge.

But this also brings new questions. How is authorship counted? Vals AI? Anthropic? Claude? The human researchers? How are contributions determined? How should review standards be updated? How is reproducibility guaranteed? These are new norms that the mathematics and AI communities must face.

VI. The future

In the short term, AI will become mathematicians’ proof engineering team. Mathematicians pose good questions, lock down theorem statements, and give strategic directions. AI handles exhaustive enumeration, combination, verification, code generation, and module merging. Already-verified methods can quickly migrate to adjacent problems. N=8 runs through, N=7 follows, and next may be N=9, N=10, or other sphere-packing, quantum many-body, or combinatorial optimization problems.

In the medium term, AI may help search for strategies, generate candidate proof skeletons, discover counterexamples, and optimize bounds. It may move from proof engineering to proof design, proposing better proof paths within a human-given framework.

In the long term, if AI can propose new conjectures, new methods, and new problems, that would be doing research on its own. Not yet.

For the research ecosystem, this event suggests that formal mathematics libraries, AI agent collaboration, and automated verification certificate engines are becoming new infrastructure. The mode of production in mathematical research may change. Humans focus more on posing good questions. AI focuses more on turning problems into verifiable proofs.

For publicity, we need qualifiers. The accurate statement is: under human-preset goals and tools, AI completed an exact formal proof of N=7 in 15 hours. AI has turned research-grade proof engineering into an automated pipeline. It is not yet doing research on its own.

Conclusion

Vals AI’s servers shut down.

The Lean file remained in the repository. A human mathematician opened it and saw the first line: the theorem statement. They had written it themselves.

Then they scrolled down: 17,895 lines of code, 47,854 declarations, all passing.

They closed the laptop and went for coffee. Tomorrow there is still N=9.