Formalizing Chemical Physics using the Lean Theorem Prover

TL;DR

This paper demonstrates how the Lean theorem prover can formalize complex chemical physics theories, ensuring mathematical rigor, clarity, and reusability across scientific frameworks.

Contribution

It introduces a formalization of chemical adsorption theories and thermodynamics using Lean, highlighting the benefits of proof verification and theory interoperability.

Findings

Formalized Langmuir and BET theories of adsorption.

Verified mathematical theorems for infinite geometric series.

Enabled reuse of proofs across different scientific theories.

Abstract

Chemical theory can be made more rigorous using the Lean theorem prover, an interactive theorem prover for complex mathematics. We formalize the Langmuir and BET theories of adsorption, making each scientific premise clear and every step of the derivations explicit. Lean's math library, mathlib, provides formally verified theorems for infinite geometries series, which are central to BET theory. While writing these proofs, Lean prompts us to include mathematical constraints that were not originally reported. We also illustrate how Lean flexibly enables the reuse of proofs that build on more complex theories through the use of functions, definitions, and structures. Finally, we construct scientific frameworks for interoperable proofs, by creating structures for classical thermodynamics and kinematics, using them to formalize gas law relationships like Boyle's Law and equations of motion underlying Newtonian mechanics, respectively. This approach can be extended to other fields, enabling the formalization of rich and complex theories in science and engineering.