我们构建了一组专门的大型语言模型代理，并展示了一种用于理论物理研究级别形式化的代理驱动工作流程，以矩阵积态基本定理的自动形式化为示例。这些代理通过结构化的数学蓝图和定期的人类审查进行协调，独立地组织和执行了完整的形式化过程。在某些陈述中，代理能够探索不属于标准文献的新证明路径。过程中，代理生成了大量之前在Mathlib中不可用的张量网络和量子信息库。作为物理应用，这一形式化也扩展到一维的对称保护拓扑相。我们发现大规模自动形式化的主要瓶颈是强制执行数学意图，并提供了对整个过程及各种细微之处的详细研究。我们将代码库发布为库 TNLean，并附带了形式化工作的 蓝图。
博主点评： 本文展示了多智能体系统在理论物理自动形式化中的潜力，尤其是在探索新证明路径方面的能力。通过建立数学蓝图和人类审查的结合，代理们能够克服传统方法的局限，推动了量子信息和张量网络领域的研究进展。未来的研究可以进一步优化代理的数学意图理解能力。