TNLean: A Lean 4 Proof of the Fundamental Theorem of Matrix Product States

What TNLean Solves and Who It Is For

TNLean addresses a specific gap: the fundamental theorem of matrix product states, a cornerstone of tensor-network theory, had no machine-checked proof. The theorem states that two tensors generate the same quantum states at every system size if and only if an invertible gauge transformation relates them. For researchers in quantum information who rely on this theorem, a formal proof removes any doubt about hidden assumptions. It is also for the formal-mathematics community, since the proof requires formalizing substantial quantum-information theory, including channel representations and quantum Perron-Frobenius theory. The library targets those who want to build on verified statements, not those seeking a computational tool. It is a proof library, not a simulator.

The Mechanism: From Tensors to Gauge Equivalence

The library defines an MPS as a function `MPSTensor d D`, where `d` is the physical dimension and `D` the bond dimension. The core result is the theorem `MPSTensor.fundamentalTheorem_singleBlock`, which states that if a tensor is injective, meaning its matrices span the full matrix algebra, and two tensors generate the same states, then they are gauge equivalent. The general case goes further: the library constructs a canonical form by decomposing an arbitrary tensor into normal blocks, and proves `MPSTensor.fundamentalTheorem_equal_canonicalForm`, which says two canonical forms generating the same states are related by a single invertible gauge. This decomposition is not trivial; it relies on a whole layer of quantum-information results that live in the companion library QICLean, which TNLean imports as a Lake dependency. The data flow is clear: QICLean provides channels, Schwarz inequalities, and spectral results; TNLean adds tensor-specific statements like transfer operators and spectral gaps.

Getting It Running: Commands and Config

The README gives a single import line: `import TNLean`. That is all you need to load the library in a Lean file, provided you have the right toolchain. The library is built on Lean 4 and Mathlib, with the latest release pinned to `v4.34.0-rc1`. To build the library yourself, the README points to `docs/getting_started.md`, which walks through building, navigating the source, and making a first contribution. The repository uses Lake as its build system, and the blueprint toolchain is configured via `tenkz.toml`, which pins the companion package `tenkz` that draws the blueprint diagrams. The workflows under `.github/workflows/` set up the Lean and blueprint toolchain using `lean-env-action` from TeXRA. If you want to reproduce the proofs, you need to match the Mathlib version exactly; using a different version may break the proofs.

What Is Actually Proved and What Is Not

The README is explicit about the state of the proofs. The fundamental theorem is proved in both its single-block and multi-block forms, and the library also proves a projective representation result for on-site symmetries of injective MPS, which is the MPS ingredient for classifying one-dimensional symmetry-protected topological phases. The quantum Wielandt inequality is proved with a spanning length of at most `D^2`, but the README notes that sharpening the bound to match literature constants is ongoing. Beyond that, several topics are in progress: parent Hamiltonians have frustration-freeness and ground-state uniqueness for injective and normal tensors, but no spectral gap estimates; matrix-product density operators are a foundation, not a complete classification; PEPS has fundamental-theorem results for normal PEPS on finite graphs. The library contains unfinished proofs marked with `sorry` and results assumed as axioms, and the badges in the README track these counts. This is honest, but it means you cannot treat every statement as fully checked.

A Genuine Limitation: The `sorry` Problem and Version Pin

The most obvious limitation is that the library is not fully complete. The README states that some files contain unfinished proofs (`sorry`) or results assumed as axioms. That means the fundamental theorem may depend on unproven statements, though the README does not say which ones. You must check the paper-gap notes at `https://sirui-lu.com/TNLean/paper-gaps/` to see exactly what is missing. Another limitation is the strict version pin: the library loads with Mathlib `v4.34.0-rc1`, and Lean's ecosystem moves fast. If you are working on a different Mathlib version, you may need to wait for a release or do a significant port. This is a common pain point for Lean libraries, and TNLean is no exception. Finally, the library is a formalization of a specific theorem, not a general tensor-network library. If you need to compute with MPS numerically, this is the wrong tool.

Alternative Approaches: QICLean and Hand Proofs

The main alternative to TNLean is not another Lean library, but the traditional approach: reading the original papers by Pérez-García, Verstraete, Wolf, and Cirac, and Cirac et al., and trusting the proofs. That approach is faster for getting intuition, but it lacks machine verification. Within the Lean ecosystem, the closest alternative is QICLean, the companion library that TNLean builds on. QICLean contains the quantum-information theory, including channel representations and quantum Perron-Frobenius theory, following Wolf's book. The difference in approach is clear: QICLean is about the general theory of quantum channels, while TNLean adds the tensor-specific layer. If you only need the channel theory, QICLean is the lighter dependency. If you need the MPS theorem, you must use TNLean. There is no other Lean library that formalizes the fundamental theorem of MPS, according to the README.

Maintenance and Upgrade Cost, and License

The project is actively maintained, with the latest push on 2026-08-18 and releases following Mathlib versions: v4.34.0-rc1, v4.32.0, and v4.31.0. This means upgrades are tied to Mathlib releases, and each new version likely requires changes to the proofs, given Lean's evolving syntax and library changes. The cost of upgrading is not trivial; you cannot just change the dependency version and expect everything to compile. The license is Apache-2.0, which is permissive for both academic and commercial use, but it does not grant any patent rights, and you should review the license terms if you plan to redistribute modifications. The README does not specify a code of conduct or contribution guidelines beyond the getting-started doc, so the maintenance model is centered on the authors and their agent-driven workflow, as described in the companion paper. For a research library, this is acceptable, but it means external contributions may not be a priority.

Editorial conclusion

Adopt TNLean if you are a researcher in quantum information or formal mathematics who needs machine-checked proofs of MPS classification results, especially the fundamental theorem and its canonical-form machinery. Do not use it as a general tensor-network library or for numerical computation, since it is a proof library with no executable code. Before adopting, verify the current counts of `sorry` and axioms in the repository, check the paper-gap notes to see which statements remain unfinished, and confirm your Lean and Mathlib versions match the pinned v4.34.0-rc1. The library's value is its precise, axiom-checked statements, not its completeness, so treat it as a reference formalization rather than a ready-made tool.

Frequently asked questions

Official sources

1. Official README
2. Project repository
3. Release notes