Benchmarking Energy Calculations Using Formal Proofs
Ejike D. Ugwuanyi, Colin T. Jones, John Velkey, Tyler R. Josephson
cond-mat.stat-mech
May 14, 2025 · v1
TL;DR
LeanLJ implements and formally verifies Lennard-Jones molecular interaction energy calculations in the Lean 4 theorem prover with executable code.
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.
Problem
Traditional validation of molecular simulations relies on open-source transparency, unit testing, and human oversight, but these approaches cannot eliminate semantic errors in scientific computing code. No formally verified framework for computing molecular interaction energies existed.
Approach
LeanLJ implements Lennard-Jones energy calculations with periodic boundaries in Lean 4, using polymorphic functions and typeclasses to bridge formal proofs over idealized Real numbers with executable programs over floating-point numbers. The approach provides proofs of correctness for coordinate wrapping, minimum image convention, and energy calculations.
Results
LeanLJ execution matches the NIST gold standard benchmarks for Lennard-Jones energy calculations while providing formal mathematical guarantees. The polymorphic strategy successfully links proofs (specialized to Real) with execution (specialized to Float) within a single codebase.
