Can eight points find their lowest-energy arrangement?
- What it is
- A paper identifies a square antiprism as the claimed best eight-point arrangement for several spherical energy models, with Lean-checked proof components.
- Who did it
- Liudmyla Kryvonos, Lukas Liehr, and Mitchell A. Taylor
- What it could mean
- If the stated formalization and certificates hold, they show how a delicate computer-assisted optimization proof can be made inspectable in a proof assistant. This does not settle energy minimization for arbitrary numbers of points.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Energy minimization for eight points on the sphere ↗See the proposed checks
Inspect the repository pin, Lean toolchain and certificate inputs in an isolated environment; trace Theorems 1.1–1.3 through the exact energy definitions and certificate statements. Do not execute manuscript-linked artifacts in this intake run.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The inspected abstract and HTML Theorems 1.1–1.3 claim that a square antiprism is the unique global minimizer for eight points under logarithmic and Coulomb energy, establish a sufficiently-large Riesz-exponent result, and state a Lean-verified computer-assisted route for the first two. The explicit proof artifacts and formalization make this a direct contribution to checking mathematics.
- Why this could matter
- Can eight points find their lowest-energy arrangement? When repelling points share a sphere, geometry decides the least-energy pattern. This paper claims that, for stated energy laws, one eight-point square antiprism wins uniquely—and makes key proof components checkable in Lean.
- If it holds up
- It would supply a reproducible formal-checking route for a precise global-optimization result in discrete geometry.
- If it does not
- A certificate, formalization boundary, or energy-family assumption would reveal exactly where the proposed optimality claim needs repair.
- Impact horizon
- Methods · Discrete geometry · Optimization · Formal verification
- Version
- submitted 2026-09-18 17:58:32 UTC
- Why we tracked it
- a fresh primary-source theorem/formalization record with a concrete Lean and certificate route. Intake does not independently validate the formalization, certificates, or the claimed all-exponent extension.
- Highest-risk dependency
- The scope is eight points and stated energy families. The abstract distinguishes Lean-verified results from an additional computer-assisted all-exponent route; neither may be generalized to arbitrary point configurations or potentials.
- Available artifacts
- arXiv exposes PDF, HTML and TeX; Section 9 names a companion Lean development and finite certificates at github.com/lukasliehr/Energy-Minimization-8-Points. No artifact was executed.
- Current boundary
- Intake record only; examination not started.