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如何通过函数、定义和结构的灵活运用，使得基于更复杂理论的证明得以重复利用。最后，我们构建了科学框架以实现可互操作的证明：为经典热力学和运动学创建了结构，并分别用于形式化波义耳定律等气体定律关系以及牛顿力学中基础的运动方程。该方法可推广至其他领域，从而实现对科学与工程中丰富而复杂理论的形式化。