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如何通过函数、定义和结构灵活地支持建立在更复杂理论之上的证明的复用。最后，我们通过为经典热力学和运动学创建结构，分别形式化了气体定律关系（如玻意耳定律）和牛顿力学中的运动方程，从而构建了可互操作证明的科学框架。该方法可推广至其他领域，实现科学与工程中丰富复杂理论的形式化。