LeanBET: Formally-verified surface area calculations in Lean

TL;DR

This paper introduces LeanBET, a formally verified pipeline for BET surface area calculations implemented in Lean 4, ensuring correctness and numerical accuracy compared to traditional methods.

Contribution

It provides the first fully executable and formally verified BET analysis workflow in Lean, covering the entire process from window enumeration to linear regression.

Findings

LeanBET agrees with the reference method to machine precision on most datasets.

The formalization covers the complete BETSI workflow, including checks and selection criteria.

The implementation demonstrates that scientific computing workflows can be both verified and numerically accurate.

Abstract

The Brunauer--Emmett--Teller (BET) method is a standard tool for estimating surface areas from adsorption isotherms, yet practical implementations involve multiple algorithmic steps whose correctness is rarely made explicit. In this work, we present a fully executable and formally verified BET analysis pipeline implemented in the Lean~4 theorem prover. Our formalization covers the complete BET Surface Identification (BETSI)-style workflow, including window enumeration, monotonicity checks, knee selection, and linear regression. We carry out computations in floating-point arithmetic and develop the corresponding correctness proofs over the real numbers, using a shared polymorphic implementation that supports both. On the proof side, we show that the regression coefficients returned by the algorithm agree with their specification-level definitions and minimize the least-squares error under the stated assumptions. We also formalize the algebraic derivation of the BET linearized expression and connect that result directly to the executable analysis pipeline. We further prove that the window enumeration is sound and complete, and that the admissibility checks and knee-based selection satisfy their formal specifications. We evaluate the implementation against the BETSI reference method on benchmark adsorption isotherms. Compared to BETSI, LeanBET agrees to machine precision for 18 of the 19 isotherms, with only a 0.03\% deviation for the UiO-66 dataset. This demonstrates that a scientific computing workflow can be built in Lean, yielding both formal verification guarantees and numerical agreement with an established Python reference implementation.