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.

翻译：Brunauer–Emmett–Teller（BET）方法是从吸附等温线估算表面积的标准工具，然而实际实现涉及多个算法步骤，其正确性鲜少被明确验证。本文提出一种在Lean~4定理证明器中实现的完全可执行且经过形式化验证的BET分析流水线。我们的形式化工作覆盖了完整的BET表面识别（BETSI）风格工作流，包括窗口枚举、单调性检查、膝点选取和线性回归。我们在浮点运算中进行计算，并基于实数开发相应的正确性证明，采用支持两者的共享多态实现。在证明方面，我们表明算法返回的回归系数与其规范层定义一致，并在既定假设下最小化最小二乘误差。我们还形式化了BET线性化表达式的代数推导，并将该结果直接关联到可执行的分析流水线。进一步证明窗口枚举是可靠且完备的，并且可接受性检查和基于膝点的选取满足其形式规范。我们在基准吸附等温线上将实现与BETSI参考方法进行了评估。与BETSI相比，LeanBET在19条等温线中的18条上达到机器精度，仅对UiO-66数据集存在0.03%的偏差。这表明可以在Lean中构建科学计算工作流，同时获得形式化验证保证，并与成熟的Python参考实现实现数值一致性。