Vals AI's ten-agent Lean proof closes the Thomson problem at N=7

Vals AI, a model-evaluation company, published a machine-checked Lean proof on September 28 that the regular pentagonal bipyramid is the lowest-energy arrangement of seven electrons on a sphere. The artifact is a single file of 17,895 lines, importing Mathlib and nothing else, public on GitHub. It was not written by Anthropic. It was written by ten Claude Sonnet 5.5 agents, deployed for about fifteen hours by Hung Tran, who documented the run on the company blog.

The caveat sits in the repository's own description: the statement is "not human-certified" and "not peer reviewed". That is the honest frame. The proof compiles and two separate kernels accept it; what that proves about AI research ability is a different and still-open question.

What the run actually produced

Tran gave the agents a Lean project and a message board, fixed two theorems in a challenge file, and proposed nine directions: porting the N=8 precedent, linear-programming bounds, splitting by combinatorial type, and building a verified certificate engine among them. The agents were free to drop or merge directions and to explain why. They wrote 1,270 messages. One agent claimed the integrator role and inlined the verified pieces into the single solution file.

The two theorems say that for every configuration of seven distinct points on the unit sphere, the Coulomb energy is at least 14.4529774142..., the energy of the bipyramid, and that equality holds only when the configuration is the bipyramid moved by a rotation, reflection or relabeling. The target enters Lean as two fixed declarations, and the proof must close both without adding assumptions.

How the proof works

The argument splits every configuration by m, the smallest pairwise inner product among the seven points. When m is at least negative 0.90, a degree-5 three-point semidefinite-programming bound, of the Bachoc-Vallentin type adapted to energy problems by Cohn and Woo, gives an energy at least E(P) plus 3e-4.

When m is below negative 0.90, five slabs covering the interval from negative 0.99 to negative 0.90 are each excluded by a three-point certificate, with a margin of about 2.6e-6 above E(P). The remaining cap, where m is at most negative 0.99, is handled by a certificate whose bound lies only 2.3e-16 below E(P). That pins any competitor into a thin tube around the bipyramid's pattern of inner products; an interval-arithmetic rigidity argument and an exact second-order local-minimality theorem then give uniqueness. The final gluing theorems are five lines long.

The certificates were found with numerical semidefinite programming and rounded to exact numbers. That distinction matters. Lean checks the numbers, so the proof does not depend on the solver that found them. The case split is not elegant, and the paper does not pretend otherwise; it is simply a way of turning a continuous minimization over seven points into finitely many exact inequalities a kernel can verify one at a time.

The verification checks

Check	What it establishes	Result
Lean build from a clean copy	Every step type-checks and every goal closes	599 s wall clock, lake build 344 s over 8,928 jobs
#print axioms on both theorems	Only Lean's standard axioms are used	propext, Classical.choice, Quot.sound
Lean Comparator	The solution proves exactly the fixed statements	"Your solution is okay!" (260 s)
Second kernel, nanoda	A separate implementation accepts the export	47,854 declarations, no errors
Negative control	The second kernel catches tampering	one changed integer makes nanoda abort

What it does not settle

The bipyramid answer for N=7 has been found numerically for decades. What was missing was the proof, because ruling out every other continuous arrangement is not the same as finding the likely one. Rigorous results exist for only a handful of small N. N=5 needed a computer-assisted proof by Schwartz, and N=8 was posted in September 2026 by Kryvonos, Liehr and Taylor, with a companion Lean development by Tooby-Smith and Zughaid that covered the N=8 case with linear-programming and three-point bounds.

Reception has been careful rather than triumphant. Jason Rute, who works on formal mathematics, called the result impressive because "the n=5 case was an ad hoc computer proof using interval arithmetic. It wasn't even clear how formalizable that proof would be in Lean." In a Reddit thread on r/singularity that scored roughly 630 points, commenters made the same point twice: the bipyramid "was basically known to be the correct answer for as long as the problem existed. It's just that no one could prove it rigorously," and "this is a solution for N=7. Not a general solution."

Both are fair. This is a runner-run artifact from a company that sells model evaluations, not an Anthropic announcement, and the models were used as agents inside a harness Tran designed. The orchestration is as much the work as the model. Reach was modest by frontier-lab standards: the announcement thread carried roughly 542 likes and 40 reposts, small numbers next to a model launch and consistent with a result aimed at a technical audience rather than a general one.

What would settle the bigger claim

A Lean proof that compiles is strong evidence, but compilation is not refereeing, and the repository says so itself. Three markers would move this from an impressive demo to a durable result: independent mathematical refereeing, upstreaming of the argument into Mathlib so that other developments can build on it, and evidence that the same method scales past small N rather than replaying a known template. Whether the case-split-plus-certificate approach stretches beyond seven points is the real test of the claim, and nobody has shown that yet. One more reason for caution: Vals AI sells model evaluations, so a favorable result also serves its own thesis that orchestrated agents can do frontier work. The five checks are a strong answer to that conflict, but they are the vendor's own checks. As we argued when an earlier AI-math result landed, the bottleneck is usually not producing a proof but finding enough mathematicians to check and absorb it.

There is no published timeline for any of that. For now the correct summary is narrow: Vals AI has a machine-checked proof for N=7, five independent checks back it, and the file's own author declined to call the statement certified. That is a real result and a modest one, and the gap between those two readings is exactly where the next round of work lives.