Multi-agent Autoformalization of Tensor Network Theory

• URL: http://arxiv.org/abs/2607.07857v1
• Date: Wed, 08 Jul 2026 18:43:33 GMT
• Title: Multi-agent Autoformalization of Tensor Network Theory
• Abstract summary: We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics.<n>The agents coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously.<n>For some statements, the agents were able to explore new proof routes that are not part of the standard literature.
• Score: 0.21847754147782886
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics, with the autoformalization of the fundamental theorem of matrix-product states as a demonstration. The agents, coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously. For some statements, the agents were able to explore new proof routes that are not part of the standard literature. Along the way the agents produced extensive tensor-network and quantum-information libraries not previously available in Mathlib, Lean's mathematical library. As a physical application, the formalization also extends towards symmetry-protected topological phases in one dimension. We find that the main bottleneck in large-scale autoformalization is enforcing mathematical intent and we provide a detailed study of the full process and various subtleties involved. We release the codebase as the library \href{https://github.com/LionSR/TNLean}{TNLean}, together with a \nChapters{}-chapter \href{https://lionsr.github.io/TNLean/blueprint/}{blueprint} of the formalization effort.

Related papers

• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  Large Language Models (LLMs) produce subtle errors that evade human detection.<n>Recent trends indicate that general-purpose LLMs now outperform smaller models explicitly fine-tuned for Lean.<n>We introduce an agentic autoformalization framework powered by general coding LLMs.
  arXiv  Detail & Related papers  (2026-06-30T05:05:03Z)
• Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance [0.3624700141426058]
  coding agents can formalize entire advanced mathematics textbooks in Lean 4.<n>We introduce a framework for evaluating the quality of agent-produced formalizations beyond compilation.<n>Our results suggest that compilation-based metrics substantially overstate formalization quality.
  arXiv  Detail & Related papers  (2026-06-12T00:45:42Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean [7.11696910077237]
  FormalScience is a human-in-the-loop agentic pipeline to produce textitsyntactically correct and textitsemantically aligned formal proofs of informal reasoning for low economic cost.<n>We construct FormalPhysics, a dataset of 200 physics problems and solutions (primarily quantum mechanics and electromagnetism) along with their Lean4 formal representations.<n>We evaluate open-source models and proprietary systems on a statement autoformalisation task on our dataset via zero-shot prompting, self-refinement with error feedback, and a novel multi-stage agentic approach.
  arXiv  Detail & Related papers  (2026-04-24T20:47:22Z)
• Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
  We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory.<n>Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library.<n>This work establishes a reusable formal foundation and opens the door for future developments in machine learning theory.
  arXiv  Detail & Related papers  (2026-02-02T16:24:53Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  We introduce MathlibLemma, the first LLM-based multi-agent system to automate the discovery and formalization of mathematical folklore lemmas.<n>We further construct the MathlibLemma benchmark, a suite of 4,028 type-checked Lean statements spanning a broad range of mathematical domains.
  arXiv  Detail & Related papers  (2026-01-30T15:24:42Z)
• Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics [25.762535169301984]
  We introduce Numina-Lean-Agent, which combines Claude Code with Numina-Lean-MCP to enable autonomous interaction with Lean.<n>Using Claude Opus 4.5 as the base model, Numina-Lean-Agent solves all problems in Putnam 2025 (12 / 12), matching the best closed-source system.
  arXiv  Detail & Related papers  (2026-01-20T14:51:45Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  We present LeanAgent, a novel lifelong learning framework for formal theorem proving.<n>LeanAgent continuously generalizes to and improves on ever-expanding mathematical knowledge.<n>It generates formal proofs for 155 theorems across 23 diverse Lean repositories.
  arXiv  Detail & Related papers  (2024-10-08T17:11:24Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  Autoformalization is the task of translating natural language mathematics into a formal language that can be verified by a program. Research paper mathematics requires large amounts of background and context. We propose an avenue towards tackling autoformalization for research-level mathematics, by breaking the task into easier and more approachable subtasks.
  arXiv  Detail & Related papers  (2023-10-12T00:50:24Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.