The Tactician's Web of Large-Scale Formal Knowledge

TL;DR

The Tactician's Web platform creates a large, interconnected dataset of formal mathematical knowledge in Coq, enabling machine learning, analytics, and proof engineering with practical agent integration.

Contribution

It introduces a comprehensive, machine-checked formal knowledge web in Coq, facilitating advanced proof automation and analysis tools.

Findings

Provides a large dataset of formal theories in Coq

Enables benchmarking of proof agents on theorems

Supports machine learning and proof engineering applications

Abstract

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.