Computer-Verified BET Analysis Using the Lean Theorem Prover.

Chemical engineering frequently requires calculations for solving problems. Because of the wide range of computational tools and methods available for performing calculations of this nature, inconsistencies between methodologies are common. For example, when adsorption datasets were sent to sixty-one different labs, there was wide variation in the corresponding BET surface area reported, despite the fact that determination of BET surface area is a well-known calculation [1]. Consider the utility then, of programs that perform calculations using functions that have provable mathematics, that are “bug free” as a result of their mathematical verification. To illustrate this concept, we use Lean 4 to write a computer-checked derivation of BET theory, and then link this derivation to functions that regress the BET parameters for a data set.

Lean 4 is a novel, multi-purpose programming language that also functions as an interactive theorem prover. We first use Lean as a theorem prover, and formally verify the derivation of the BET adsorption theory. This proof is first presented in [2], originally implemented in an earlier version of the Lean interactive theorem prover. Proofs in Lean 4 are not identical to executable computing programs, which can be separately defined as functions. Not all computing functions can have proofs written on them, if they are strictly typed to function with floating-point numbers. This is due to the disjoint relationship between Real numbers and floats. Reals can be the subject of proofs, but because they potentially have infinite decimal digits, they cannot be computed or displayed by computer systems. Instead, scientific computing uses floats to perform actual calculations, but proofs about floats are not the same as proofs about reals; even a + b - b = a is not true for all floats. To make verified scientific computing possible in Lean, we introduce a method using polymorphic functions to connect proofs about real-valued functions to computations using the same functions with float-valued inputs. We use the developed code to analyze datasets from [1] performing BET regression, and compare our formally-verified results to those previously reported.

[1] Osterrieth, Johannes W. M., et al. “How Reproducible Are Surface Areas Calculated from the BET Equation?” Advanced Materials, vol. 34, no. 27, 23 May 2022, p. 2201502, https://doi.org/10.1002/adma.202201502.

[2] Bobbin, Maxwell P, et al. “Formalizing Chemical Physics Using the Lean Theorem Prover.” ArXiv (Cornell University), 21 Oct. 2022, https://doi.org/10.48550/arxiv.2210.12150.