The Tactician's Web of Large-Scale Formal Knowledge
Not on the map. Why?
Abstract (arXiv)
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.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Builds on 11 of its 42 references that are in the map. First posted on arXiv 5 Jan 2024.
Builds on
11 of 42 references.
References · 11
- 2017Attention Is All You Needcited by 60,361
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
- 2022Formal Mathematics Statement Curriculum Learningcited by 142
- 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
- 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 109
- 2018GamePad: A Learning Environment for Theorem Provingcited by 48
- 2019Generating Correctness Proofs with Neural Networkscited by 37
- 2017HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Provingcited by 26
- 2020The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coqcited by 24
- 2022Passport: Improving Automated Formal Verification Using Identifierscited by 19
- 2021Online Machine Learning Techniques for Coq: A Comparisoncited by 7
Built on by
Citing papers per year: 2025: 1.
1 paper.