Benchmarking Energy Calculations Using Formal Proofs

Abstract

Traditional approaches for validating molecular simulations rely on making software open source and transparent, incorporating unit testing, and generally employing human oversight. We propose an approach that eliminates software errors using formal logic, providing proofs of correctness. We use the Lean theorem prover and programming language to create a rigorous, mathematically verified framework for computing molecular interaction energies. We demonstrate this in LeanLJ, a package of functions, proofs, and code execution software that implements Lennard Jones energy calculations in periodic boundaries. We introduce a strategy that uses polymorphic functions and typeclasses to bridge formal proofs (about idealized Real numbers) and executable programs (over floating point numbers). Execution of LeanLJ matches the current gold standard NIST benchmarks, while providing even stronger guarantees, given LeanLJ's grounding in formal mathematics. This approach can be extended to formally verified molecular simulations, in particular, and formally verified scientific computing software, in general. Keywords: Formal verification, Lean 4, molecular simulations, functional programming.

arXiv commentMolecular Physics (2025)

References in corpus (7)

• The Lennard-Jones potential: when (not) to use it
• The Lennard Jones Potential Revisited -- Analytical Expressions for Vibrational Effects in Cubic and Hexagonal Close-Packed Lattices
• A Brief Review on Results and Computational Algorithms for Minimizing the Lennard-Jones Potential
• Formalization of physics index notation in Lean 4
• Workflow for investigating thermodynamic, structural and energy properties of condensed polymer systems from Molecular Dynamics
• Integrated Lennard-Jones Potential between a Sphere and a Thin Rod
• HepLean: Digitalising high energy physics