Formalizing chemical physics using the Lean theorem prover
dc.contributor.author | P. Bobbin, Maxwell | |
dc.contributor.author | Sharlin, Samiha | |
dc.contributor.author | Feyzishendi, Parivash | |
dc.contributor.author | Hong Dang, An | |
dc.contributor.author | M. Wraback, Catherine | |
dc.contributor.author | R. Josephson, Tyler | |
dc.date.accessioned | 2024-04-10T19:05:42Z | |
dc.date.available | 2024-04-10T19:05:42Z | |
dc.date.issued | 2023-11-16 | |
dc.description.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. | |
dc.description.sponsorship | We 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.uri | https://pubs.rsc.org/en/content/articlelanding/2024/dd/d3dd00077j | |
dc.format.extent | 17 pages | |
dc.genre | journal articles | |
dc.identifier | doi:10.13016/m2qaep-coet | |
dc.identifier.citation | P. 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.uri | https://doi.org/10.1039/D3DD00077J | |
dc.identifier.uri | http://hdl.handle.net/11603/32982 | |
dc.language.iso | en_US | |
dc.publisher | Royal Society of Chemistry | |
dc.relation.isAvailableAt | The University of Maryland, Baltimore County (UMBC) | |
dc.relation.ispartof | UMBC Faculty Collection | |
dc.relation.ispartof | UMBC Chemical, Biochemical & Environmental Engineering Department | |
dc.relation.ispartof | UMBC Computer Science and Electrical Engineering Department | |
dc.relation.ispartof | UMBC Student Collection | |
dc.rights | CC BY 3.0 DEED Attribution 3.0 Unported | |
dc.rights.uri | https://creativecommons.org/licenses/by/3.0/ | |
dc.title | Formalizing chemical physics using the Lean theorem prover | |
dc.type | Text | |
dcterms.creator | https://orcid.org/0000-0002-6379-9206 | |
dcterms.creator | https://orcid.org/0000-0002-0100-0227 |