Chemical theory can be made more rigorous using the Lean theorem prover, an interactive theorem prover for complex mathematics. We formalize the Langmuir and BET 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.

翻译：化学理论可通过Lean定理证明器（一种适用于复杂数学的交互式定理证明器）变得更加严谨。我们形式化了吸附理论中的Langmuir和BET理论，使每个科学前提清晰明确，推导的每一步都具体化。Lean的数学库mathlib提供了已验证的无穷级数定理，这些定理是BET理论的核心。在编写这些证明的过程中，Lean提示我们包含最初未报告的一些数学约束。我们还展示了Lean如何通过函数、定义和结构，灵活地复用构建于更复杂理论基础上的证明。最后，我们构建了可互操作的证明科学框架：为经典热力学和运动学建立结构，并分别将其用于形式化波义耳定律等气体定律关系以及牛顿力学背后的运动方程。这种方法可扩展到其他领域，从而实现对科学与工程中丰富复杂理论的形式化。