# Formalization of physics index notation in Lean 4

arXiv: https://arxiv.org/abs/2411.07667 · HTML: https://mlsanity.com/paper/2411.07667/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Nov 2024.

## Built on by (most cited first, 4 of 4)

- [LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4](https://mlsanity.com/paper/2507.14722/) (2025)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [NanoProof: Open and Efficient Automated Theorem Proving in Lean 4](https://mlsanity.com/paper/2610.11605/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

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.