CAREER: Automated Reasoning to Advance Chemical Theory

With joint support from the Chemical Theory, Models and Computational Methods (CTMC) program in the Division of Chemistry (CHE) and the Office of Advanced Cyberinfrastructure (OAC), Tyler Josephson of the University of Maryland, Baltimore County (UMBC) is developing a new approach to writing code in computational chemistry. It is important when testing new algorithms that they be coded correctly. Lean is a programming language that can help check whether math proofs are correct. Josephson's lab, the AI & Theory-Oriented Molecular Science (ATOMS) Lab at UMBC, will use and teach others to use Lean to write derivations and simulation software in Lean, ensuring that the math and code is correct. They will develop LeanMD (Lean-molecular dynamics) software for simulating the motion of molecules, that is designed to be free of bugs and math errors. This project will expand to SciLib, a community-sourced library of proofs across all fields of science and engineering. Others may use these proofs to probe the scientific literature and verify proofs of their own, accelerating the discovery of new theories. Community college outreach activities and recruitment of transfer students for undergraduate research will support a diverse STEM (science, technology, engineering and mathematics) workforce. Cross-disciplinary collaboration with the developers of Lean at Microsoft Research is anticipated to foster student learning and professional development. Computer scientists use interactive theorem provers to verify mathematics and software, but these are scarcely used in scientific computing. Lean, a modern theorem prover and programming language developed by Microsoft Research (MSR), is designed to enable mathematicians to define high-level mathematical objects and prove statements about them. Tyler Josephson's research group, the AI & Theory-Oriented Molecular Science (ATOMS) Lab, is exploring how to translate the mathematics of classical mechanics and molecular dynamics (MD) into Lean code (defining the Hamiltonian and Newton's equations of motion, as well as computable expressions like the Verlet algorithm, and proving relationships between them), and use these to build LeanMD, formally-verified software for MD. This is the first step toward creating SciLib, an open-source library of proofs in science and engineering, similar to mathlib, Lean's community-sourced mathematics library. A large database of proofs can be used to evaluate large language models (LLMs) for auto-completing proofs (with verification provided by the Lean compiler), translating informal science into formal proofs (and the reverse), and for generating, proving, and explaining new theories. To teach Lean to scientists and engineers, the ATOMS Lab is planning annual training workshops, with engagement measured by members' sustained contributions to SciLib, as well as interactive online games, built in Lean, that introduce theorem proving and the Lean language to non-mathematicians. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.