Issue 2, 2024

Formalizing chemical physics using the Lean theorem prover

Abstract

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.

Graphical abstract: Formalizing chemical physics using the Lean theorem prover

Supplementary files

Transparent peer review

To support increased transparency, we offer authors the option to publish the peer review history alongside their article.

View this article’s peer review history

Article information

Article type
Paper
Submitted
26 Apr 2023
Accepted
08 Nov 2023
First published
16 Nov 2023
This article is Open Access
Creative Commons BY license

Digital Discovery, 2024,3, 264-280

Formalizing chemical physics using the Lean theorem prover

M. P. Bobbin, S. Sharlin, P. Feyzishendi, A. H. Dang, C. M. Wraback and T. R. Josephson, Digital Discovery, 2024, 3, 264 DOI: 10.1039/D3DD00077J

This article is licensed under a Creative Commons Attribution 3.0 Unported Licence. You can use material from this article in other publications without requesting further permissions from the RSC, provided that the correct acknowledgement is given.

Read more about how to correctly acknowledge RSC content.

Social activity

Spotlight

Advertisements