Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | https://arxiv.org/abs/2509.13142 |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908542732075008 |
|---|---|
| author | Bobbin, Maxwell P. Jones, Colin Velkey, John Josephson, Tyler R. |
| author_facet | Bobbin, Maxwell P. Jones, Colin Velkey, John Josephson, Tyler R. |
| contents | Dimensional analysis is fundamental to the formulation and validation of physical laws, ensuring that equations are dimensionally homogeneous and scientifically meaningful. In this work, we use Lean 4 to formalize the mathematics of dimensional analysis. We define physical dimensions as mappings from base dimensions to exponents, prove that they form an Abelian group under multiplication, and implement derived dimensions and dimensional homogeneity theorems. Building on this foundation, we introduce a definition of physical variables that combines numeric values with dimensions, extend the framework to incorporate SI base units and fundamental constants, and implement the Buckingham Pi Theorem. Finally, we demonstrate the approach on an example: the Lennard-Jones potential, where our framework enforces dimensional consistency and enables formal proofs of physical properties such as zero-energy separation and the force law. This work establishes a reusable, formally verified framework for dimensional analysis in Lean, providing a foundation for future libraries in formalized science and a pathway toward scientific computing environments with built-in guarantees of dimensional correctness. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_13142 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formalizing dimensional analysis using the Lean theorem prover Bobbin, Maxwell P. Jones, Colin Velkey, John Josephson, Tyler R. Chemical Physics Dimensional analysis is fundamental to the formulation and validation of physical laws, ensuring that equations are dimensionally homogeneous and scientifically meaningful. In this work, we use Lean 4 to formalize the mathematics of dimensional analysis. We define physical dimensions as mappings from base dimensions to exponents, prove that they form an Abelian group under multiplication, and implement derived dimensions and dimensional homogeneity theorems. Building on this foundation, we introduce a definition of physical variables that combines numeric values with dimensions, extend the framework to incorporate SI base units and fundamental constants, and implement the Buckingham Pi Theorem. Finally, we demonstrate the approach on an example: the Lennard-Jones potential, where our framework enforces dimensional consistency and enables formal proofs of physical properties such as zero-energy separation and the force law. This work establishes a reusable, formally verified framework for dimensional analysis in Lean, providing a foundation for future libraries in formalized science and a pathway toward scientific computing environments with built-in guarantees of dimensional correctness. |
| title | Formalizing dimensional analysis using the Lean theorem prover |
| topic | Chemical Physics |
| url | https://arxiv.org/abs/2509.13142 |