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.

在这篇论文中，我们介绍了Tactician's Web平台，它提供了一个大型的、相互连接的、经过机器验证的数学知识网络，方便地用于机器学习、分析和证明工程。该平台构建在Coq证明助手之上，导出了一个包含广泛形式理论的数据集，以定义、定理、证明项、策略和证明状态的网络形式呈现，并提供了人类可读的文本形式。与Coq的紧密整合使得可以将证明代理作为实用工具提供给证明工程师。

战略家的大规模形式知识网络