# Multi-agent Autoformalization of Tensor Network Theory

> A multi-agent LLM system autonomously formalized the fundamental theorem of matrix-product states in Lean 4, discovering a novel proof via Skolem-Noether and building a 227,000-line tensor-network library.

- **Source:** [arXiv](https://arxiv.org/abs/2607.07857)
- **Published:** 2026-08-17
- **Permalink:** https://picx.dev/p/23YNki
- **Whiteboard:** https://picx.dev/p/23YNki/image

## Summary

## Summary (Overview)

- **First autonomous multi-agent formalization** of a research-level theorem in theoretical physics: the fundamental theorem of matrix-product states (FT-MPS), verified in the Lean 4 proof assistant.
- **Team of six specialized LLM agents** (orchestrator, proof writer, library scout, simplifier, blueprint synchronizer, reviewer) coordinated via a shared mathematical blueprint and persistent memory, with only intermittent human oversight.
- **Novel proof discovery**: The system autonomously proved the injective case of FT-MPS via the Skolem-Noether theorem, an approach not standard in the literature.
- **Extensive library development**: Produced TNLean, a Lean 4 tensor-network library of ~227,000 lines, including quantum information infrastructure (completely positive maps, quantum Perron-Frobenius theory, quantum Wielandt bound).
- **Physical application**: Extended the formalization to symmetry-protected topological (SPT) phases, proving a cohomological invariant theorem for injective symmetric MPS.

---

## Introduction and Theoretical Foundation

### Background

Proof assistants (e.g., Lean 4, Coq) verify mathematical arguments step-by-step. While AI systems have automated proofs for competition problems and isolated lemmas, research-level formalizations (e.g., Liquid Tensor Experiment, Fermat's Last Theorem) have remained primarily human-led efforts requiring months or years of expert work.

**Key challenge**: Theoretical physics results often lack the mathematical rigor of pure mathematics, requiring formalization to "fill in" informal reasoning with rigorous, machine-checkable statements.

### The Fundamental Theorem of Matrix-Product States (FT-MPS)

A translationally invariant matrix-product state (MPS) on $N$ sites with periodic boundary conditions is parameterized by a rank-3 tensor $A$:

$$
|\psi_N(A)\rangle = \sum_{i_1,\dots,i_N=0}^{d-1} \operatorname{tr}\left(A^{i_1} A^{i_2} \dots A^{i_N}\right) |i_1 \dots i_N\rangle \tag{1}
$$

where $A = \sum_{i=0}^{d-1} A^i |i\rangle$ and $A^i \in M_D(\mathbb{C})$ (the space of $D \times D$ complex matrices). Here $d$ is the local Hilbert-space dimension and $D$ is the bond dimension.

**Key definitions:**
- **Transfer operator**: $E_A: M_D(\mathbb{C}) \to M_D(\mathbb{C})$ defined by $E_A(X) = \sum_{i=0}^{d-1} A^i X (A^i)^\dagger$
- **Normal tensor**: $A$ is normal if $E_A$ has spectral radius 1 and a unique eigenvalue $\lambda$ with $|\lambda| = 1$
- **Canonical form (CF)**: $A^i = \bigoplus_{k=1}^{r} \mu_k A_k^i$ where $\mu_k \in \mathbb{C}$ and $A_k$ are normal tensors

**Theorem 1 (Fundamental Theorem of MPS, equal case)**: Let $A$ and $B$ be two tensors in CF. Then $A$ and $B$ generate the same MPV family, $|\psi_N(A)\rangle = |\psi_N(B)\rangle$ for every $N \geq 1$, if and only if there exists an invertible matrix $X$ such that for all $i = 0, 1, \dots, d-1$:

$$
B^i = X A^i X^{-1} \tag{2}
$$

---

## Methodology

### Multi-Agent Architecture

The system (built on TeXRA software) employs **six specialized agent roles**:

| Agent | Function | Model Tier |
|-------|----------|------------|
| **Orchestrator** | Assigns tasks, combines results, manages workflow | Most capable |
| **Proof Writer (lean)** | Constructs Lean proofs, responds to type-checking feedback | Most capable, most expensive |
| **Library Scout (leanSearch)** | Surveys Mathlib for existing lemmas and results | Inexpensive |
| **Simplifier (leanSimplifier)** | Refactors code, extracts reusable strategies, retires failed attempts | Inexpensive |
| **Blueprint Synchronizer (leanBlueprint)** | Keeps blueprint prose aligned with Lean declarations | Inexpensive |
| **Reviewer** | Automated cross-checking of claims against literature | Runs automatically |

### Coordination Patterns

Three recurring orchestration patterns:
1. **Parallel dispatch** (Fig. 4a): Independent subtasks $T_1, \dots, T_r$ dispatched to workers on disjoint scopes
2. **Scout-then-prove** (Fig. 4b): Inexpensive scout surveys library, emits design memo; expensive prover invoked only after feasible route identified
3. **Review-repair cycles** (Fig. 4c): Reviewer flags issues, fixer applies patches; loop terminates on acceptance or after 5 iterations

### Blueprint and Persistent Memory

- **Blueprint**: A human-readable mathematical specification linking definitions, theorem statements, and dependencies to Lean code. Serves as the interface between literature and formalization.
- **Persistent memory**: Records scouting results, proof strategies, counterexamples, and technique notes across sessions (bounded working periods).
- **Human oversight**: Strategic only (not tactical) — the supervisor reviews the blueprint, sets mathematical intent, but never writes Lean code or chooses proof tactics.

---

## Empirical Validation / Results

### Formalization Scale

- **Core development**: ~62,000 lines of code, 2,300 declarations, 233 files
- **Full TNLean library**: ~227,000 lines
- **Blueprint**: 12 chapters, 150 pages
- **Cost**: $20,206 total API cost ($5,548 for FT-MPS alone)
- **Verification**: Every step of the FT-MPS proof chain verified with no remaining `sorry` markers

### Key Findings on Challenges

**1. Weakening of theorems**: The agents initially proved FT-MPS under a "doubly stochastic gauge" assumption (requiring both unital and trace-preserving transfer operators simultaneously, which is impossible for generic MPS tensors). This produced a formally correct but narrower theorem.

**2. Finite vs. asymptotic limits**: Early attempts replaced finite-$N$ MPV comparisons with asymptotic norm comparisons, which proved statements with wrong hypotheses. The correct proof keeps comparisons at fixed finite $N$.

**3. Edge cases**: Proof assistants require explicit handling of edge cases ($D=0$, $N=0$) that carry no physical meaning; adding assumptions $D \geq 1$ and $N \geq 1$ removed large irrelevant proof branches.

**4. Blueprint-Lean misalignment**: Several reviews found discrepancies where Lean statements were correct but blueprint prose had drifted.

### Novel Proof Route

The injective case of FT-MPS was proven via the **Skolem-Noether theorem** (about automorphisms of central simple algebras), leveraging Mathlib's existing ring-theory library. This is not the standard approach in the MPS literature.

### Physical Application: SPT Phases

**Theorem 2 (A cohomological invariant from injective symmetric MPS)**: Let $A$ be an injective MPS tensor of bond dimension $D \geq 1$, and $U: G \to GL_d(\mathbb{C})$ an onsite linear representation of a finite group $G$. Define $\widetilde{A}_g^i := \sum_j U(g)_{ij} A^j$. If $A$ is invariant under $U$ (i.e., $|\psi_N(A)\rangle = |\psi_N(\widetilde{A}_g)\rangle$ for all $g \in G$, $N \geq 1$), then for each $g \in G$ there is an invertible matrix $X(g) \in GL_D(\mathbb{C})$, unique up to a nonzero scalar, such that:

$$
\widetilde{A}_g^i = X(g) A^i X(g)^{-1} \tag{3}
$$

With $\rho(g) := X(g^{-1})$, the maps $\rho(g)$ form a projective representation with 2-cocycle $\omega(g,h) \in \mathbb{C}^\times$. The cohomology class $[\omega] \in H^2(G, \mathbb{C}^\times)$ is unchanged by rescaling gauges and depends only on the symmetric tensor $A$ with on-site action $U$.

---

## Theoretical and Practical Implications

### For Autoformalization

- **Mathematical intent is the main bottleneck**: The paper demonstrates that "enforcing the correct mathematical intent" — not individual lemma proofs — is the primary challenge in large-scale autoformalization. Lean checks proofs but not statement choices.
- **Definitions are more dangerous than proofs**: Confirms Buzzard's warning in a concrete setting; incorrect definitions propagate errors through hundreds of downstream lemmas.
- **Context window constraints**: No LLM context window can hold source literature + blueprint + growing formal library simultaneously, necessitating the multi-agent split with persistent memory.
- **Blueprint as essential infrastructure**: Review and blueprint synchronization are not auxiliary but central to correctness at scale.

### For Physics

- **TNLean library** provides verified infrastructure for tensor-network theory, quantum information (CP maps, Perron-Frobenius theory), and quantum many-body physics.
- **SPT classification**: The formalization of the cohomological invariant connects FT-MPS to the classification of 1D bosonic SPT phases, with natural extensions to parent Hamiltonians and gapped paths.

### Cost-Effectiveness

The recorded cost of $20,206 (with FT-MPS alone at $5,548) represents a significant reduction compared to traditional human-led formalization efforts spanning months or years.

---

## Conclusion

This work demonstrates that a team of specialized AI agents, coordinated through a shared blueprint with sporadic human supervision, can autonomously formalize research-level theorems in theoretical physics. The FT-MPS formalization succeeded with:

- **Novel proof discovery** (Skolem-Noether route for injective case)
- **Extensive library development** (TNLean, ~227,000 lines)
- **Physical applications** (SPT phase classification)

**Key insight**: The main bottleneck is not proof search but **enforcing mathematical intent** — ensuring the formalized statement matches the intended theorem. This requires blueprint review, automated cross-checking, and strategic human oversight.

**Future directions**:
- Formalization of FT-MPS with boundaries, higher-dimensional tensor-network states, parent Hamiltonians, matrix-product operators
- Larger targets: low individual degree test, MIP$^*$ = RE theorem
- The released technique notes and distilled memory files are project-independent and can seed other autoformalization efforts

---

_Markdown view of https://picx.dev/p/23YNki, served by PicX — AI-generated visual whiteboard summaries of research papers._