The Tactician's Web of Large-Scale Formal Knowledge
This addresses the need for accessible formal knowledge resources for researchers and engineers in automated theorem proving and machine learning, though it is incremental as it builds on existing Coq infrastructure.
The paper introduces The Tactician's Web, a platform that provides a large-scale, interconnected dataset of formal mathematical knowledge from the Coq proof assistant, enabling machine learning and proof engineering applications by offering data in both semantic graph and human-readable formats.
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.