形式化验证张量网络理论的多智能体自动形式化Lu 等（2026）构建了一支专门化的大语言模型智能体团队，在 Lean/Mathlib 中完成了矩阵乘积态基本定理的研究级自动形式化演示，构建了 TNLean 库并延伸至一维对称保护拓扑相 2026-07-12