(416h) Formal Proofs in the Chemical Sciences Using the Lean Theorem Prover

In contrast to derivations that are simply hand-written or typeset in a research article, a formalized proof is a computer-verified sequence of steps logically relating the axioms of a problem to a conjecture to be proved.

Mathematicians have formalized tens of thousands of proofs in self-consistent libraries[1], but formal theorem proving has received less attention in science and engineering.

Formalizing proofs in the chemical sciences is worthwhile for at least two reasons. Firstly, formal proofs enable more rigorous science. Formalized proofs are guaranteed to be valid, and require every assumption to be laid out in transparent, mathematical precision. Scientists can focus on the assumptions and definitions, trusting that any proved conjectures necessarily follow. Secondly, formal proofs are machine-readable and interpretable. This is enabling automated problem solving in pure mathematics, for example, artificial intelligence tools have solved problems from the International Math Olympiad[2].

To formalize proofs in the chemical sciences, we propose to use the Lean language and theorem prover[1]. It can express the advanced math required in our most elegant proofs (e.g. statistical, quantum, and fluid mechanics), which sometimes require (random variables, partial differential equations, and N-dimensional integrals).

We show how a few prototypical proofs can be developed in Lean, including the kinetic derivation of the Langmuir adsorption model[3], as well as the BET theory of multilayer adsorption, which invokes two infinite geometric series in its proof[4]. By checking the conditions of each lemma used in the proof, Lean guarantees that the proof is valid and consistent with all the other math in its database.

1. L. de Moura, et al.. The Lean Theorem Prover. 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015
2. S. Polu, et al.. Formal Mathematics Statement Curriculum Learning, arXiv:2202.01344 [cs], 2022
3. I. Langmuir, THE ADSORPTION OF GASES ON PLANE SURFACES OF GLASS, MICA AND PLATINUM, JACS 40, 1361, 1918
4. S. Brunauer, P. H. Emmett, E. Teller. Adsorption of Gases in Multimolecular Layers, JACS 60, 309, 1938