News · 2026-10-01

Vals publishes a two-kernel-checked artifact for the seven-point Thomson problem

Hung Tran of Vals AI published an account of a Claude-agent-generated formal proof for the seven-point Thomson problem on September 28. The public repository reports acceptance by Lean and a separately implemented checking kernel, alongside checks against fixed theorem statements. It also explicitly says the statement is not human-certified and the work is not peer reviewed, preserving an important boundary around the claim.

Key facts

• Tran reports ten Claude Sonnet 5.5 agents working for about 15 hours.
• The agents exchanged 1,270 messages while building the artifact.
• The account was published September 28, 2026.
• The primary sources are Tran’s Vals write-up and the public proof repository.

The Thomson problem asks where repelling points should sit on a sphere to minimize their total interaction energy. For seven points, the claimed arrangement is a pentagonal bipyramid: five points around an equatorial ring and one at each pole. The reported formal theorems concern that arrangement’s optimality and uniqueness, allowing rotations, reflections, and relabeling of the points.

A physical analogy is seven tiny charged beads constrained to a hollow globe. Moving one bead changes its distance from every other bead, so an arrangement that looks balanced need not be globally best. Finding a low-energy arrangement numerically is easier than proving no other arrangement beats it. The formal artifact is about closing that gap for the stated seven-point problem.

According to Tran’s account, the agents received two fixed Lean theorem statements and were asked to prove them. That setup matters. If a system can silently change the goal while constructing its proof, successful compilation may say little about the intended challenge. Fixed statements and a comparator provide a way to check that the final artifact still addresses the declared targets.

The proof uses several mathematical techniques rather than a simple search over positions. Tran describes splitting the possibilities according to the smallest pairwise inner product. Away from nearly opposite pairs, the argument uses semidefinite bounds. Other regions are covered with certificates, followed by interval arithmetic and an exact argument establishing local minimality and rigidity. Those are descriptions from the author’s write-up, not an independent reconstruction in this synthesis.

Numerical optimization helped find coefficients for certificates. The account says those certificates were converted to exact data and checked in Lean. That distinction is valuable: a floating-point experiment can suggest that a bound holds, while a formal checker requires precisely stated objects and justified inequalities. Numerical discovery and formal validation play different roles in the reported workflow.

The repository reports a 17,895-line Lean file that builds from a clean copy using only Lean’s standard axioms. It says Lean’s Comparator accepts the proof against the fixed statements, and nanoda, a separately implemented kernel, accepts the exported artifact. The repository also describes a negative control in which changing a certificate integer causes nanoda to reject the export.

An independent checker is like having a second calculator verify a long computation using its own implementation. Agreement reduces reliance on one program’s checking code. The corrupted-certificate test additionally shows that the alternate checker rejects at least one intentionally wrong artifact. Neither step, however, certifies that every informal interpretation of the mathematical problem has been encoded correctly.

The project states the limit unusually plainly: “Statement not human-certified. Not peer reviewed.” That is a short quote from the repository, and it should travel with the headline. A proof assistant validates the formal derivation under stated assumptions. Human review can still be needed to check definitions, intended scope, prior work, and whether the formalized statement is the mathematical result readers believe has been established.

This release arrives alongside AGMAI’s recommendations for publishing AI-generated mathematics with artifacts, disclosure, and support for understanding. The Vals repository makes several layers inspectable, which is stronger than a bare announcement. Yet the dossier did not independently rerun the build or obtain a mathematician’s certification of the statement. Its status remains an author-reported machine-checked artifact with explicit unresolved review work.

A separate source mix-up also needs correction. A September 30 Reddit item linked Scientific American’s percolation report, concerning continuity of transitions in dimensions three through ten. That is not this seven-point optimization problem. The ten-agent detail cannot be imported into the percolation story simply because both involve AI and mathematics.

The useful conclusion is specific: Vals has released a substantial artifact with fixed-target checking, a second kernel, and an honest review-status label. Ground Truth’s earlier verification-lag reporting explains why that layered description matters. Readers can inspect what was checked without turning the remaining human-certification gap into either automatic rejection or a claim of fully settled mathematics.

Primary source, verified: read the paper →

Ground Truth. (2026, October 1). Vals publishes a two-kernel-checked artifact for the seven-point Thomson problem. Ground Truth. https://groundtruth.day/news/vals-thomson-n7-lean-proof-artifact.html

@misc{groundtruth:vals-thomson-n7-lean-proof-artifact,
  title  = {Vals publishes a two-kernel-checked artifact for the seven-point Thomson problem},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {oct},
  url    = {https://groundtruth.day/news/vals-thomson-n7-lean-proof-artifact.html}
}

Topics: mathematics · agents · verification · ai-science · formal-methods