Formalizing chemical physics using the Lean theorem prover

dc.contributor.authorP. Bobbin, Maxwell
dc.contributor.authorSharlin, Samiha
dc.contributor.authorFeyzishendi, Parivash
dc.contributor.authorHong Dang, An
dc.contributor.authorM. Wraback, Catherine
dc.contributor.authorR. Josephson, Tyler
dc.date.accessioned2024-04-10T19:05:42Z
dc.date.available2024-04-10T19:05:42Z
dc.date.issued2023-11-16
dc.description.abstractInteractive 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.
dc.description.sponsorshipWe are grateful to the Lean prover community and contributors of mathlib on whose work this project is built. We especially thank Kevin Buzzard, Patrick Massot, Tomas Skrivan, Eric Wieser, and Andrew Yang for helpful comments and discussions around our proof structure and suggestions for improvement. We thank Charles Fox, Mauricio Collares, and Ruben Van de Velde for helping with the website. We thank two anonymous peer reviewers, as well as Rose Bohrer, John Keith, and Ben Payne for reading the manuscript and providing helpful feedback. This material is based upon work supported by the National Science Foundation under Grant No. (NSF #2138938), as well as startup funds from the University of Maryland, Baltimore County.
dc.description.urihttps://pubs.rsc.org/en/content/articlelanding/2024/dd/d3dd00077j
dc.format.extent17 pages
dc.genrejournal articles
dc.identifierdoi:10.13016/m2qaep-coet
dc.identifier.citationP. Bobbin, Maxwell, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M. Wraback, and Tyler R. Josephson. “Formalizing Chemical Physics Using the Lean Theorem Prover.” Digital Discovery 3, no. 2 (2024): 264–80. https://doi.org/10.1039/D3DD00077J.
dc.identifier.urihttps://doi.org/10.1039/D3DD00077J
dc.identifier.urihttp://hdl.handle.net/11603/32982
dc.language.isoen_US
dc.publisherRoyal Society of Chemistry
dc.relation.isAvailableAtThe University of Maryland, Baltimore County (UMBC)
dc.relation.ispartofUMBC Faculty Collection
dc.relation.ispartofUMBC Chemical, Biochemical & Environmental Engineering Department
dc.relation.ispartofUMBC Computer Science and Electrical Engineering Department
dc.relation.ispartofUMBC Student Collection
dc.rightsCC BY 3.0 DEED Attribution 3.0 Unported
dc.rights.urihttps://creativecommons.org/licenses/by/3.0/
dc.titleFormalizing chemical physics using the Lean theorem prover
dc.typeText
dcterms.creatorhttps://orcid.org/0000-0002-6379-9206
dcterms.creatorhttps://orcid.org/0000-0002-0100-0227

Files

Original bundle

Now showing 1 - 2 of 2
Loading...
Thumbnail Image
Name:
d3dd00077j.pdf
Size:
1.64 MB
Format:
Adobe Portable Document Format
Loading...
Thumbnail Image
Name:
d3dd00077j1.pdf
Size:
517.3 KB
Format:
Adobe Portable Document Format