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

TL;DR

This paper introduces a computer-assisted proof framework that converts numerical geometry optimization results into rigorous mathematical proofs, demonstrated on carbon nanotubes and Lennard-Jones crystals.

Contribution

The authors develop a novel framework for transforming standard simulations into formal proofs of geometric structures in atomistic models.

Findings

Proven bounds on nanotube diameter, bond lengths, and angles.

Validated existence of perfect and defective crystal configurations.

Demonstrated diameter oscillations induced by caps in nanotubes.

Abstract

We present a framework based on computer-assisted proofs that turns standard 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 (fcc) lattice and provide computer-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.