3 papers
cs.LO2026
LeanBET: Formally-verified surface area calculations in Lean
Ejike D. Ugwuanyi, Colin T. Jones, John Velkey +1
The Brunauer--Emmett--Teller (BET) method is a standard tool for estimating surface areas from adsorption isotherms, yet practical implementations involve multiple algorithmic step…
physics.chem-ph2025
Formalizing dimensional analysis using the Lean theorem prover
Maxwell P. Bobbin, Colin Jones, John Velkey +1
Dimensional analysis is fundamental to the formulation and validation of physical laws, ensuring that equations are dimensionally homogeneous and scientifically meaningful. In this…
cond-mat.stat-mech2025
Benchmarking Energy Calculations Using Formal Proofs
Ejike D. Ugwuanyi, Colin T. Jones, John Velkey +1
Traditional approaches for validating molecular simulations rely on making software open source and transparent, incorporating unit testing, and generally employing human oversight…