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 Theorem 验证器可以使化学理论更加严格, 这是一种互动理论, 可以证明复杂的数学。 我们正式确定Langmuir和BET吸收理论, 使每个科学前提和衍生的每一个步骤都清楚明晰。 Lean的数学图书馆Mathlib 提供了无限的地貌序列正式核实的理论, 这对理论来说至关重要。 在写这些证据时, Lean 促使我们把原先没有报告的数学限制包括在内。 我们还说明Lian 如何通过使用功能、 定义和结构, 使建立在更复杂的理论之上的证明得以重新使用。 最后, 我们通过建立古典热力学和运动学的结构, 利用它们来正式确定气体法关系, 如 Boyle 法 和 Newtonian 机械基础的动作等式。 这种方法可以推广到其他领域, 使科学和工程的丰富和复杂的理论正规化。