利用Lean定理证明器形式化化学物理
摘要：使用Lean证明器，一种用于复杂数学的交互式证明器，可以使化学理论更加严格。我们对Langmuir和BET吸附理论进行形式化，使得每个科学假设都清晰，并且每个推导步骤都是明确的。Lean的数学库mathlib为无限几何级数提供了经过正式验证的定理，这对BET理论至关重要。在编写这些证明时，Lean提示我们要包含原始报告中未报告的数学限制。我们还展示了Lean如何通过函数、定义和结构灵活地支持基于更复杂理论的证明的重复使用。最后，我们通过为经典热力学和运动学创建结构，并使用它们来形式化像Boyle定律和支持牛顿力学的运动方程这样的气体定律关系，构建了科学框架以实现互操作证明。这种方法可以扩展到其他领域，使得能够形式化科学和工程中丰富而复杂的理论。
作者：Maxwell P. Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M. Wraback, and Tyler R. Josephson
论文ID：2210.12150
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-17