Search for: All records

Interactive theorem provers are computer programs that check whether mathematical statements are correct. We show how the mathematics of theories in chemical physics can be written in the language of the Lean theorem prover, allowing chemical theory to be made even more rigorous and providing insight into the mathematics behind a theory. We use Lean to precisely define the assumptions and derivations of the Langmuir and BET theories of adsorption. We can also go further and create a network of definitions that build off of each other. This allows us to define a common basis for equations of motion or thermodynamics and derive many statements about them, like the kinematic equations of motion or gas laws such as Boyle's law. This approach could be extended beyond chemistry, and we propose the creation of a library of formally-proven theories in all fields of science. Furthermore, the rigorous logic of theorem provers complements the generative capabilities of AI models that generate code; we anticipate their integration to be valuable for automating the discovery of new scientific theories. 

As molecular modeling and simulation techniques become increasingly important sources of thermophysical property and phase equilibrium data, the ability to assess the robustness of that data becomes more critical. Recently, the use of the compressibility factor (Z) has been suggested as a metric for testing the quality of simulation data for vapor−liquid equilibria (VLE). Here, we analyze predicted VLE data from the transferable potentials for phase equilibria (TraPPE) database and show that, apart from data entry or typographical errors, Z will always be well-behaved in Gibbs ensemble Monte Carlo (GEMC) simulations even when the simulations are not sufficiently equilibrated. However, this is not true for grand canonical Monte Carlo simulations. When the pressure is calculated from the internal forces, then pressure and density are strongly correlated for the vapor phase and, for GEMC simulations, it is recommended to treat Z as an instantaneous mechanical property. From analysis of the TraPPE VLE data, we propose a complementary metric based on the predicted vapor pressures at three neighboring temperatures and their deviation from a local Clausius−Clapeyron fit.