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:

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