{"total":21,"rows":[{"id":"2404.09939","title":"A Survey on Deep Learning for Theorem Proving","created":"2024-04-15","cited_by_count":57,"area":null},{"id":"2303.04488","title":"Magnushammer: A Transformer-Based Approach to Premise Selection","created":"2023-03-08","cited_by_count":50,"area":null},{"id":"2102.09756","title":"TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning","created":"2021-02-19","cited_by_count":37,"area":null},{"id":"2106.03906","title":"Learning to Guide a Saturation-Based Theorem Prover","created":"2021-06-07","cited_by_count":15,"area":null},{"id":"2401.02949","title":"Graph2Tac: Online Representation Learning of Formal Math Concepts","created":"2024-01-05","cited_by_count":15,"area":null},{"id":"2112.10664","title":"Proving Theorems using Incremental Learning and Hindsight Experience Replay","created":"2021-12-20","cited_by_count":13,"area":null},{"id":"2102.03529","title":"Vampire With a Brain Is a Good ITP Hammer","created":"2021-02-06","cited_by_count":10,"area":null},{"id":"2304.00994","title":"Machine-Learned Premise Selection for Lean","created":"2023-03-17","cited_by_count":10,"area":null},{"id":"2105.14706","title":"The Role of Entropy in Guiding a Connection Prover","created":"2021-05-31","cited_by_count":8,"area":null},{"id":"2107.06750","title":"Fast and Slow Enigmas and Parental Guidance","created":"2021-07-14","cited_by_count":8,"area":null},{"id":"2205.01981","title":"The Isabelle ENIGMA","created":"2022-05-04","cited_by_count":8,"area":null},{"id":"2107.10034","title":"Learning Theorem Proving Components","created":"2021-07-21","cited_by_count":7,"area":null},{"id":"2303.06686","title":"MizAR 60 for Mizar 50","created":"2023-03-12","cited_by_count":6,"area":null},{"id":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","cited_by_count":6,"area":null},{"id":"2101.09142","title":"A Study of Continuous Vector Representationsfor Theorem Proving","created":"2021-01-22","cited_by_count":4,"area":null},{"id":"2210.03590","title":"Machine Learning Meets The Herbrand Universe","created":"2022-10-07","cited_by_count":3,"area":null},{"id":"2403.03401","title":"BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving","created":"2024-03-06","cited_by_count":2,"area":null},{"id":"2204.02737","title":"Adversarial Learning to Reason in an Arbitrary Logic","created":"2022-04-06","cited_by_count":1,"area":null},{"id":"2406.17762","title":"Solving Hard Mizar Problems with Instantiation and Strategy Invention","created":"2024-06-25","cited_by_count":1,"area":null},{"id":"2503.07792","title":"Efficient Neural Clause-Selection Reinforcement","created":"2025-03-10","cited_by_count":0,"area":null},{"id":"2609.31029","title":"Governed Deduction: Policy-Grounded Premise Authorization Beyond Relevance","created":"2026-09-25","cited_by_count":0,"area":null}],"next_cursor":null}