A Lean Proof of the Thomson Problem for Seven Electrons
Source
vals.ai
Date
Why it matters
Shows how far coding agents can go on a continuous-geometry theorem that previously needed computer-assisted proofs for small cases. Useful calibrationHow well a model's confidence matches reality — a calibrated model saying "90% sure" is right about 90% of the time.Full definition → for anyone using agents on formal verification.
Key takeaways · AI-distilled
Ten Claude Sonnet 5.5 agents sharing a message board produced, in about 15 hours and 1,270 messages, a Lean proof that the pentagonal bipyramid is the unique minimum-energy arrangement of seven charges on a sphere (the Thomson problem for N=7).
The proof splits configurations by their smallest pairwise inner product, using three-point semidefinite-programming bounds for most cases and an interval-arithmetic rigidity argument plus an exact second-order local-minimality theorem near the bipyramid.
Certificates were found by numerical SDP and rounded to exact numbers checked in Lean's kernel, so the result does not depend on the solver; it builds on the N=8 proofs posted in September 2026.
The 17,895-line file was checked with a clean build, an axiom audit, Lean Comparator against the fixed statements, and a second kernel (nanoda), which a negative control showed rejects a one-integer change.
Terms in this piece · Glossary
calibration — How well a model's confidence matches reality — a calibrated model saying "90% sure" is right about 90% of the time.
