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.

翻译：物理学界依赖指标表示法来高效处理各类张量。本文介绍了在交互式定理证明器Lean 4中首个经过形式化验证的指标表示法实现。通过将指标表示法集成到Lean中，我们弥合了传统物理符号与形式化验证工具之间的鸿沟，使得物理学家在Lean中编写和证明结果变得更加便捷。我们也为利用AI工具证明物理学中与张量相关的结果开辟了一条新途径。在实现背后，我们的工作利用了范畴论的一种新颖应用。