Formalizing Chemical Theory using the Lean Theorem Prover
| dc.contributor.author | Bobbin, Maxwell P. | |
| dc.contributor.author | Sharlin, Samiha | |
| dc.contributor.author | Feyzishendi, Parivash | |
| dc.contributor.author | Dang, An Hong | |
| dc.contributor.author | Wraback, Catherine M. | |
| dc.contributor.author | Josephson, Tyler R. | |
| dc.date.accessioned | 2022-11-10T18:32:29Z | |
| dc.date.available | 2022-11-10T18:32:29Z | |
| dc.date.issued | 2022-10-28 | |
| dc.description.abstract | Chemical theory can be made more rigorous using the Lean theorem prover, an interactive theorem prover for complex mathematics. We formalize the Langmuir [1] and BET [2] theories of adsorption, making each scientific premise clear and every step of the derivations explicit. Lean’s math library, mathlib, provides formally-verified theorems for infinite geometries series, which are central to BET theory. While writing these proofs, Lean prompts us to include mathematical constraints that were not originally reported. We also illustrate how Lean flexibly enables the reuse of proofs that build on more complex theories through the use of functions, definitions, and structures. Finally, we construct scientific frameworks for interoperable proofs, by creating structures for classical thermodynamics and kinematics, using them to formalize gas law relationships like Boyle’s Law and equations of motion underlying Newtonian mechanics, respectively. This approach can be extended to other fields, enabling the formalization of rich and complex theories in science and engineering. | en_US |
| 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. This material is based upon work supported by the National Science Foundation under Grant No. (NSF #218938), as well as startup funds from the University of Maryland, Baltimore County. | en_US |
| dc.description.uri | https://arxiv.org/abs/2210.12150 | en_US |
| dc.format.extent | 22 pages | en_US |
| dc.genre | journal articles | en_US |
| dc.genre | preprints | en_US |
| dc.identifier | doi:10.13016/m2tvxg-hxfg | |
| dc.identifier.uri | https://doi.org/10.48550/arXiv.2210.12150 | |
| dc.identifier.uri | http://hdl.handle.net/11603/26301 | |
| dc.language.iso | en_US | en_US |
| dc.relation.isAvailableAt | The University of Maryland, Baltimore County (UMBC) | |
| dc.relation.ispartof | UMBC Computer Science and Electrical Engineering Department Collection | |
| dc.relation.ispartof | UMBC Faculty Collection | |
| dc.relation.ispartof | UMBC Student Collection | |
| dc.relation.ispartof | UMBC Chemical, Biochemical & Environmental Engineering Department | |
| dc.relation.ispartof | UMBC Center for Women in Technology (CWIT) | |
| dc.rights | This item is likely protected under Title 17 of the U.S. Copyright Law. Unless on a Creative Commons license, for uses protected by Copyright Law, contact the copyright holder or the author. | en_US |
| dc.rights | Attribution 4.0 International (CC BY 4.0) | * |
| dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | * |
| dc.title | Formalizing Chemical Theory using the Lean Theorem Prover | en_US |
| dc.type | Text | en_US |
| dcterms.creator | https://orcid.org/0000-0002-6379-9206 | en_US |
| dcterms.creator | https://orcid.org/0000-0002-0100-0227 | en_US |