Tactician's Web of Large-Scale Formal Knowledge

This dataset contains machine-readable data extracted by Tactician from formal knowledge encoded in the Coq Proof Assistant. It includes definitions, theorems, proof terms and tactical proofs presented both as Coq's default textual format and a graph format. The entire known universe of formal knowledge in Coq is encoded as a single interconnected graph of mathematical concepts where all knowledge is faithfully and unambiguously encoded. The dataset is intended for machine learning, analysis and general proof engineering purposes. In addition to exploring this offline dataset, it is also possible to interact directly with Coq in the same data format through Tactician's API. See the README.md file for more information.