(11i) Benchmarking Molecular Simulations Using Formal Proofs

When developing new methods for molecular simulation, eliminating bugs can be challenging. Programming languages like Python, FORTRAN, and Julia flag syntax errors, but don't (and cannot) catch errors in math or program logic - these must be rooted out by human experts. These issues can be managed by following best practices in software development (such as writing tests alongside the program), but even these do not guarantee that code is correct.

Lean is a new programming language developed for writing and automatically checking the logic of math proofs. We can translate derivations in science and engineering into math proofs, and use Lean's capabilities as a theorem prover to verify that the logic of the derivation is correct [1]. Lean also can be used to write executable programs, though this requires adopting a functional programming style, replacing for and while loops with recursive functions. These functions can be the subject of proofs that verify their properties. We use this approach to develop energy calculations for Lennard-Jones particles in periodic boundaries, and compare our implementation to the NIST benchmark [2]. The Lean implementation is a stronger benchmark than that available by NIST because the underlying mathematics have been formally verified.

[1] Bobbin, M.P., et al., “Formalizing Chemical Physics Using the Lean Theorem Prover,” Digital Discovery, 3, 16 Nov 2024, p 264–280, https://doi.org/10.1039/D3DD00077J.

[2] Shen, V.K., Siderius, D.W., Krekelberg, W.P., and Hatch, H.W., Eds., NIST Standard Reference Simulation Website, http://doi.org/10.18434/T4M88Q.