Computer-Assisted Proofs for Geometry Optimization: From Crystallization to Carbon Nanotubes

We present a framework based on computer-assisted proofs that turns geometry optimization simulations for atomistic structures into mathematical proofs. Starting from a numerically computed approximation of a local minimizer or saddle point, we use validated numerical computations to prove the existence of a critical point of the potential energy close to this approximation. We demonstrate this framework in two settings. In the first, we study capped carbon nanotubes modeled as minimizers of carbon interatomic potentials (harmonic, Tersoff, and a Huber potential) and obtain proven bounds on tube diameter, bond lengths, and bond angles. In particular, we show that caps induce diameter oscillations along the tube. As a second application, we consider a finite Lennard–Jones crystal in a face-centered cubic lattice and provide computer-assisted proofs of a local minimizer representing the perfect crystal, a local minimizer with a single vacancy defect, and a saddle point that connects two single-vacancy configurations on the energy landscape.