# Graph2Tac: Online Representation Learning of Formal Math Concepts arXiv: https://arxiv.org/abs/2401.02949 · HTML: https://mlsanity.com/paper/2401.02949/ ## Key facts - Cited by 15 papers in the map (data through 14 Oct 2026). - Builds on 24 of its 46 references that are in the map. - First posted on arXiv 5 Jan 2024. ## Builds on (most cited first, 24 of 24) - [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023) - [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020) - [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022) - [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021) - [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019) - [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022) - [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019) - [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023) - [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018) - [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019) - [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017) - [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020) - [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019) - [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020) - [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013) - [TF-GNN: Graph Neural Networks in TensorFlow](https://mlsanity.com/paper/2207.03522/) (2022) - [Passport: Improving Automated Formal Verification Using Identifiers](https://mlsanity.com/paper/2204.10370/) (2022) - [Learning to Reason with HOL4 tactics](https://mlsanity.com/paper/1804.00595/) (2018) - [Machine-Learned Premise Selection for Lean](https://mlsanity.com/paper/2304.00994/) (2023) - [Tactic Learning and Proving for the Coq Proof Assistant](https://mlsanity.com/paper/2003.09140/) (2020) - [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022) - [Online Machine Learning Techniques for Coq: A Comparison](https://mlsanity.com/paper/2104.05207/) (2021) - [SEPIA: Search for Proofs Using Inferred Automata](https://mlsanity.com/paper/1505.07987/) (2015) - [Machine Learning of Coq Proof Guidance: First Experiments](https://mlsanity.com/paper/1410.5467/) (2014) ## Built on by (most cited first, 15 of 15) - [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024) - [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024) - [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024) - [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024) - [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024) - [Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning](https://mlsanity.com/paper/2502.13834/) (2025) - [Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification](https://mlsanity.com/paper/2410.19940/) (2024) - [Premise Selection for a Lean Hammer](https://mlsanity.com/paper/2506.07477/) (2025) - [Learning Structure-Aware Representations of Dependent Types](https://mlsanity.com/paper/2402.02104/) (2024) - [Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving](https://mlsanity.com/paper/2503.09730/) (2025) - [Neuro-Symbolic AI for Cybersecurity: State of the Art, Challenges, and Opportunities](https://mlsanity.com/paper/2509.06921/) (2025) - [ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving](https://mlsanity.com/paper/2502.04671/) (2025) - [What are the Right Symmetries for Formal Theorem Proving?](https://mlsanity.com/paper/2605.22257/) (2026) - [Harnessing Code Agents for Automatic Software Verification](https://mlsanity.com/paper/2607.06341/) (2026) - [PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs](https://mlsanity.com/paper/2608.12762/) (2026) ## Abstract (arXiv) In proof assistants, the physical proximity between two formal mathematical concepts is a strong predictor of their mutual relevance. Furthermore, lemmas with close proximity regularly exhibit similar proof structures. We show that this locality property can be exploited through online learning techniques to obtain solving agents that far surpass offline learners when asked to prove theorems in an unseen mathematical setting. We extensively benchmark two such online solvers implemented in the Tactician platform for the Coq proof assistant: First, Tactician's online k-nearest neighbor solver, which can learn from recent proofs, shows a 1.72× improvement in theorems proved over an offline equivalent. Second, we introduce a graph neural network, Graph2Tac, with a novel approach to build hierarchical representations for new definitions. Graph2Tac's online definition task realizes a 1.5× improvement in theorems solved over an offline baseline. The k-NN and Graph2Tac solvers rely on orthogonal online data, making them highly complementary. Their combination improves 1.27× over their individual performances. Both solvers outperform all other general-purpose provers for Coq, including CoqHammer, Proverbot9001, and a transformer baseline by at least 1.48× and are available for practical use by end-users.