We built a team of specialized large language model agents and presented an agent-driven workflow for research-level formalization in theoretical physics, demonstrating the autoformalization of the fundamental theorem of matrix-product states. The agents, coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously. For some statements, the agents explored new proof routes not part of the standard literature. Along the way, they produced extensive tensor-network and quantum-information libraries not previously available in Mathlib. The formalization also extends to symmetry-protected topological phases in one dimension. We identified that the main bottleneck in large-scale autoformalization is enforcing mathematical intent and provided a detailed study of the full process and its subtleties. We released the codebase as the library TNLean, along with a formalization effort blueprint.
Blogger's Review: This article showcases the potential of multi-agent systems in the autoformalization of theoretical physics, particularly in their ability to explore new proof paths. By combining mathematical blueprints with human review, the agents overcome the limitations of traditional methods, advancing research in quantum information and tensor networks. Future studies could further optimize the agents' understanding of mathematical intent.