Formalization of physics index notation in Lean 4

TL;DR

This paper introduces the first formally verified implementation of index notation in the interactive theorem prover Lean 4, which bridges the gap between traditional physics notation and formal verification tools, and opens up a new avenue through which AI tools can be used to prove results related to tensors in physics.

Abstract

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.

Figures (1)

• Figure 1: Overview of the implementation of index notation in Lean. The solid lines represent formally verified parts of the implementation.