Vals AI's 10 Claude Sonnet 5.5 Agents Crack a 17,895-Line Math Proof
Vals AI explains how ten Claude agents produced a Lean proof for seven electrons on a sphere, and names which cases should fall next.
- Vals AI published the method behind their Lean proof that seven electrons on a sphere form a pentagonal bipyramid.
- Ten Claude Sonnet 5.5 agents produced a 17,895-line Lean proof in roughly 15 hours.
- The core recipe: three-point semidefinite bound plus case splits on inner products, closed by a local Hessian argument.
- Three-point bound shrinks the pair-angle gap by 13 to 25x at symmetric N=9 and 10.
- Vals predicts N=10 then N=9 fall next with the same machinery.
- N=32 (icosahedron plus dodecahedron) is posted as an open Prove2Me challenge needing a new idea.
Place N unit charges on a sphere and minimize their Coulomb energy, E = ∑i<j 1/|xi − xj|. For N = 7, the minimizer is a pentagonal bipyramid: two antipodal poles and a regular pentagon around the equator. Numerical optimization finds that configuration quickly. A global proof must rule out every competing arrangement.
After releasing a formal proof for N = 7, Vals AI published a detailed account of its method and its prospects for larger cases. Vals says ten Claude Sonnet 5.5 agents produced the 17,895-line Lean proof in about 15 hours. Lean’s kernel checks the resulting proof term, while exact and interval-verified certificates control the numerical steps.
The project has also opened challenges for N = 9, 10, and 32, with the first two presented as plausible extensions of the same proof architecture.
The missing 0.4%
A standard proof strategy constructs a lower bound that applies to every configuration and matches the candidate’s energy. Delsarte-style linear programs derive such bounds from the angles, or equivalently the inner products, between pairs of points. For the 12 vertices of an icosahedron, the pairwise bound reaches the exact energy.
For N = 7, the pairwise bound is about 14.40, while the pentagonal bipyramid has energy near 14.45. The roughly 0.4% gap leaves room for a hypothetical configuration with lower energy. Pairwise information permits collections of angles that cannot arise from seven points on a sphere, so the relaxation cannot eliminate every false candidate.
Three-point bounds tighten the relaxation by coupling three inner products at once. Each triple must have a positive semidefinite Gram matrix, which encodes whether three unit vectors with those mutual angles can exist. Branching then divides the remaining configuration space into regions where these stronger constraints can certify a sharper lower bound.
Branch, certify, finish locally
The exposition organizes the proof as a branch-and-bound computation over pairwise inner products:
- Branch. Divide configuration space using inequalities on inner products, such as a minimum angular separation between every pair.
- Certify. Solve a three-point semidefinite program on each region. A semidefinite program optimizes a linear expression while requiring specified matrices to remain positive semidefinite.
- Prune. Discard any region whose certified lower bound exceeds the pentagonal bipyramid’s energy.
- Finish locally. Reduce the surviving region to a neighborhood of the candidate, then use the Hessian to prove the energy rises in every non-rotational direction.
The three-point method originated in work by Bachoc and Vallentin and was adapted to energy minimization by Cohn and Woo. It retains the polynomial tests available to the classical pairwise program and adds matrix constraints, so its best lower bound is at least as strong as the pairwise result.
Symmetry predicts the workload
Vals’s comparisons suggest that the number of distinct inner products in the candidate configuration predicts the three-point method’s performance. The pairwise relaxation changes relatively steadily with N. The three-point relaxation improves sharply for symmetric configurations with few distinct inner products: at N = 9 and 10, it reduces the pairwise gap by factors of roughly 13 to 25. At the lower-symmetry cases N = 11 and 13, it cuts the gap by only about half.
The local proof also depends on curvature near the candidate. After removing the zero modes caused by rotation, the smallest Hessian eigenvalue for N = 7 is 0.0092. Such weak curvature requires tight interval estimates because the energy rises slowly along the flattest direction. The corresponding eigenvalues for N = 9 and 10 are 10 to 16 times larger, giving the local argument wider numerical margins.
Three targets, three bottlenecks
| Case | Candidate | Evidence | Remaining obstacle |
|---|---|---|---|
| N = 10 | Capped square antiprism | Antipodal poles allow the N = 7 case split to transfer. The three-point relative gap is about 1.7 × 10−4. | The optimal height lacks a closed form, so the local proof needs a high-precision interval enclosure. |
| N = 9 | Tricapped triangular prism | It has the smallest three-point gap among the listed open cases and a comparatively stiff Hessian. | Without an antipodal pair, the proof may need the N=8 Lean proof strategy: choose a branch boundary where the bound becomes exact and use the equality conditions to constrain survivors. |
| N = 32 | Icosahedron plus dodecahedron | The candidate combines the vertices of two dual polyhedra. | The three-point bound barely improves the pairwise result, and no known branch cut closes the gap. The case needs a stronger relaxation or a new decomposition. |
From one proof to a reusable pipeline
The broader contribution is a workflow that combines numerical discovery, semidefinite certificates, branch-and-bound decomposition, local Hessian estimates, and Lean verification. The N = 7 proof shows that language-model agents can fill a large formal scaffold while Lean checks each step.
Vals identifies branch selection as the main automation target. Reusing the formal infrastructure across values of N could shift more work toward generating and checking candidate-specific certificates, although each case still requires suitable cuts, exact or interval-enclosed parameters, and a local curvature argument.
Developers and researchers can find the exact Lean statements for N = 9, 10, and 32 on the Prove2Me mission. Vals says it will publish an account of any successful N = 32 proof and credit its author.
Comments
