A Lean 4 and Mathlib effort to put tensor-network theory and quantum many-body results on a machine-checked foundation. Several supporting results are formalized from scratch, including Brouwer’s fixed-point theorem and the existence of mixed Nash equilibria, which serve as building blocks for the larger development.
A team of specialized LLM agents, coordinated through a structured mathematical blueprint and periodic human review, autonomously formalized the fundamental theorem of matrix-product states and extended the development toward symmetry-protected topological phases in one dimension. Described with Erickson Tjoa and J. Ignacio Cirac in Multi-agent Autoformalization of Tensor Network Theory↗ (arXiv:2607.07857).