2025 AIChE Annual Meeting

(336c) Formalizing Thermodynamic Properties from the Helmholtz Free Energy using Lean

Authors

Tyler Josephson - Presenter, University of Maryland, Baltimore County
Ismail Alkhatib, Khalifa University of Science and Technology (KU)
The Helmholtz free energy is a convenient basis for empirical and theory-based equations of state, as properties can be derived via partial derivatives. Typically, the derivation of the equation of state, as well as the mathematics involved in connecting the equation of state to the properties, are done by hand. We propose an alternative approach, based on formal verification using the Lean theorem prover and programming language, which verifies the mathematics of each step.

This study presents a mathematically grounded formalization of the Helmholtz free energy and its associated thermodynamic properties using Lean, a proof assistant based on dependent type theory which allows the formal encoding of mathematical structures, logical inference rules, and physical models. Our aim is to develop a reproducible, logically sound framework for thermodynamic reasoning, bridging the gap between physics, formal logic, and computer verification. We formalize the concept of the canonical ensemble and link it to the Helmholtz free energy, as the fundamental thermodynamic property, and we define the subsequent links to key thermodynamic properties including 1st and 2nd derivative properties in addition to identities for isothermal and adiabatic processes. We start with modeling the ideal gas, noting that this approach can be extended to a variety of models for real fluids.

Through this work, we demonstrate that modern theorem proving tools such as Lean can play a transformative role in the development and application of physical theory. By uniting physical insight with logical precision, this formalization reinforces the connection between foundational science and practical engineering in a manner that is reproducible, verifiable, and future-ready.