The Tactician's Web is a platform offering a large web of strongly interconnected, machine-checked, formal mathematical knowledge conveniently packaged for machine learning, analytics, and proof engineering. Built on top of the Coq proof assistant, the platform exports a dataset containing a wide variety of formal theories, presented as a web of definitions, theorems, proof terms, tactics, and proof states. Theories are encoded both as a semantic graph (rendered below) and as human-readable text, each with a unique set of advantages and disadvantages. Proving agents may interact with Coq through the same rich data representation and can be automatically benchmarked on a set of theorems. Tight integration with Coq provides the unique possibility to make agents available to proof engineers as practical tools.

翻译：战术家网络是一个提供大规模、强互联、机器验证的形式化数学知识平台，这些知识被便捷地打包用于机器学习、分析与证明工程。该平台构建于Coq证明助手之上，导出一个包含多种形式化理论的数据集，以定义、定理、证明项、策略及证明状态构成的网络形式呈现。这些理论既被编码为语义图（如下所示），也被编码为人类可读文本，各具独特优势与局限性。证明代理可通过相同的丰富数据表示与Coq交互，并能在定理集上自动进行基准测试。与Coq的紧密集成提供了独特可能性，使代理能作为实用工具供证明工程师使用。