Benchmarking energy calculations using formal proofs

ED Ugwuanyi and CT Jones and J Velkey and TR Josephson, MOLECULAR PHYSICS, 123 (2025).

DOI: 10.1080/00268976.2025.2539421

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 type classes to bridge formal proofs (about idealised 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.

Return to Publications page