Multi-agent Autoformalization of Tensor Network Theory¶

🕒 Published (v1): 2026-07-08 18:43 UTC · Source: Arxiv · link

Why this paper was selected

Multi-agent autoformalization of physics theory; demonstrates frontier agent capability on formal reasoning

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

A team of specialized LLM agents, coordinated through a shared mathematical blueprint and periodic human review, autonomously formalized the fundamental theorem of matrix-product states (FT-MPS) in Lean 4, producing the TNLean library (~227,000 lines). The work reveals that enforcing correct mathematical intent—not individual proof search—is the primary bottleneck in large-scale agentic autoformalization. Agents also autonomously discovered a non-standard proof route for the injective case via the Skolem-Noether theorem.

Problem¶

Research-level formalization in theoretical physics has remained almost entirely human-led, requiring expert teams over months or years. Existing AI proof systems target competition problems or isolated lemmas, not the multi-layered infrastructure needed for physics theorems (transfer operators, CP maps, spectral theory), which also requires making implicit physical conventions mathematically explicit. The key open question is how far an agent-driven system can carry an end-to-end formalization of a research-grade physics theorem.

Method¶

Five specialized LLM agents are orchestrated within the TeXRA framework: - An orchestrator decomposes the overall proof into subtasks and dispatches them to sub-agents. - A leanSearch agent scouts Mathlib for reusable lemmas. - A lean agent writes and closes Lean 4 proofs. - A leanBlueprint agent maintains mechanical link consistency (every \lean reference resolves, every \leanok flags a closed proof via checkdecls). - An automated reviewer agent checks two semantic correspondences: blueprint-vs-Lean (does the Lean theorem prove the stated result?) and literature-vs-Lean (are hypotheses no stronger than the source?). Mismatches return statements for restatement and re-proof. - A simplifier agent periodically refactors proof files and retires failed attempts.

Coordination is mediated by a blueprint—a human-readable LaTeX specification with machine-readable links to Lean declarations—that records unified notation, canonical-form assumptions, and normalization conventions across sessions. A persistent memory carries corrected conventions and rejected proof routes between sessions, compensating for bounded LLM context windows. Six rounds of human blueprint review fed reports back to the orchestrator, which dispatched corrections autonomously without tactical guidance.

Key Contributions¶

First autonomous multi-agent formalization of a research-level mathematical-physics theorem (FT-MPS) in Lean 4, with zero sorry placeholders in the core argument.
TNLean library: ~227,000 lines, 2,300 declarations, 233 files, extending Mathlib with tensor-network and quantum-information infrastructure (CP maps, quantum Perron-Frobenius theory, quantum Wielandt bound).
A 12-chapter, 150-page formalization blueprint linking every step to Lean code.
Autonomous discovery of a non-standard proof of the injective FT-MPS case via the Skolem-Noether theorem (not in the standard literature).
Formalization of Theorem 2: a cohomological invariant $[\omega] \in H^2(G, \mathbb{C}^\times)$ classifying 1D symmetry-protected topological (SPT) phases, derived autonomously after agents were supplied the relevant reference.
Release of distilled memory files and technique notes documenting rejected formulations, required hypotheses, and deviations from informal presentations.

Results¶

FT-MPS fully formalized with no sorry markers; estimated API cost $5,548 for FT-MPS alone, $20,206 for the full TNLean library.
Agents autonomously proved the injective FT-MPS case via Skolem-Noether without being directed to that route.
Multi-block general case (canonical form after blocking) required supplying arXiv LaTeX sources of primary references; agents then regenerated the proof strategy autonomously.
Agents autonomously pursued and completed the SPT cohomological invariant formalization after being supplied one additional reference.
Six human review rounds were sufficient to steer the full formalization; human intervention was strategic (identifying wrong statement), not tactical (not specifying how to fix it).
Statements occupying a few lines in the literature required several hundred lines of Lean code.

Limitations¶

Mathematical intent enforcement is the dominant bottleneck: Lean verifies proofs but not the choice of statement; agents produced formally correct but narrower theorems (e.g., doubly-stochastic gauge assumption, asymptotic vs. finite-$N$ comparison) requiring human identification.
Bounded context windows prevent a single agent session from simultaneously holding source papers, the growing Lean library, proof state, and intended theorem statement; task splitting and blueprint/memory are required workarounds, not solutions.
Agent instruction following is unreliable at scale; periodic blueprint review and rejection tracking are necessary to prevent agents from drifting back to incorrect formulations.
The full 1D SPT classification (symmetric parent Hamiltonians, gapped paths) is not formalized; only the cohomological invariant piece is completed.
Cost ($20K+ API) and the need for sporadic expert human review limit accessibility and full autonomy.
The multi-agent system is built on TeXRA; portability to other frameworks is undemonstrated.

Relevance to Agentic AI / LLM Agents¶

This paper is a rare, large-scale empirical study of a multi-agent system operating at the frontier of a technical domain (formal mathematics/physics), providing concrete findings on where current LLM agents fail: not at individual reasoning steps but at maintaining a coherent global specification across long-horizon tasks. The blueprint-as-shared-memory architecture and the reviewer-as-consistency-checker pattern are directly applicable design principles for any agentic system that must coordinate multiple LLMs over a complex, multi-session project. The finding that "definitions are more dangerous than proofs" in agentic autoformalization—i.e., statement drift is harder to detect than proof errors—is an important warning for agentic systems applied to any domain with precise formal specifications (code generation, legal reasoning, scientific modeling). The autonomous discovery of a non-standard proof route (Skolem-Noether) also supports the hypothesis that LLM agent pools can surface cross-domain connections beyond what single-model or human-only approaches typically explore.