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.
Code releasing soon at sirui-lu.com/TNLean.