Formalization of physics index notation in Lean 4
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929588975697920 |
|---|---|
| author | Tooby-Smith, Joseph |
| author_facet | Tooby-Smith, Joseph |
| contents | The physics community relies on index notation to effectively manipulate types of tensors. This paper introduces the first formally verified implementation of index notation in the interactive theorem prover Lean 4. By integrating index notation into Lean, we bridge the gap between traditional physics notation and formal verification tools, making it more accessible for physicists to write and prove results within Lean. We also open up a new avenue through which AI tools can be used to prove results related to tensors in physics. Behind the scenes our implementation leverages a novel application of category theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_07667 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Formalization of physics index notation in Lean 4 Tooby-Smith, Joseph Logic in Computer Science High Energy Physics - Phenomenology High Energy Physics - Theory The physics community relies on index notation to effectively manipulate types of tensors. This paper introduces the first formally verified implementation of index notation in the interactive theorem prover Lean 4. By integrating index notation into Lean, we bridge the gap between traditional physics notation and formal verification tools, making it more accessible for physicists to write and prove results within Lean. We also open up a new avenue through which AI tools can be used to prove results related to tensors in physics. Behind the scenes our implementation leverages a novel application of category theory. |
| title | Formalization of physics index notation in Lean 4 |
| topic | Logic in Computer Science High Energy Physics - Phenomenology High Energy Physics - Theory |
| url | https://arxiv.org/abs/2411.07667 |