Formalization of Scientific Theories with Interactive Theorem Proving

Interactive theorem provers offer an exciting new way for human-computer interaction in the field of formal proofs. These programs enable humans to feed formal proofs to a computer, which verifies the validity of the proof in real time. We show how the mathematics of scientific theories can be made more rigorous using these theorem provers. We used the Lean Theorem Prover, with its accompanying mathematics library, mathlib, to formalize the Langmuir and BET theories of adsorption. We noticed that the logic required for formal mechanics is more meticulous than what the original paper by Brunauer er. al. We also note a lot of hidden assumptions that scientist subconsciously make that need to be specified for Lean. Discovering and implanting these assumptions have increased insight into the properties of some theories, which was a wonderful surprise for us. However, these interactive theorem provers can do more than prove individual theorems, they can link together theorems and mathematical objects. Using this capability, we show a way to begin formalizing the fields of classical thermodynamics and kinematics. Along with these two fields, we have begun laying the framework to formalize statistical mechanics, with mathlibs newly defined probability section. Just as the Lean theorem prover has a community of mathematicians working to expand mathlib, we hope to create a similar community and library of formalized scientific theorems.