 Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2024 |
 Towards Neural Synthesis for SMT-Assisted Proof-Oriented ProgrammingInternational Conference on Software Engineering (ICSE), 2024 |
 Considerations on Approaches and Metrics in Automated Theorem
Generation/Finding in GeometryAutomated Deduction in Geometry (ADG), 2024 |
 A Survey of Reasoning with Foundation Models Jiankai Sun Chuanyang Zheng Enze Xie Zhengying Liu Ruihang Chu ...Xipeng Qiu Yi-Chen Guo Hui Xiong Qun Liu Zhenguo Li |
 LeanDojo: Theorem Proving with Retrieval-Augmented Language ModelsNeural Information Processing Systems (NeurIPS), 2023 |
 MizAR 60 for Mizar 50International Conference on Interactive Theorem Proving (ITP), 2023 |
 CoProver: A Recommender System for Proof ConstructionInternational Conference on Intelligent Computer Mathematics (CICM), 2023 |
 A Survey of Deep Learning for Mathematical ReasoningAnnual Meeting of the Association for Computational Linguistics (ACL), 2022 |
 Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal
ProofsInternational Conference on Learning Representations (ICLR), 2022 |
 Autoformalization with Large Language ModelsNeural Information Processing Systems (NeurIPS), 2022 |
 HyperTree Proof Search for Neural Theorem ProvingNeural Information Processing Systems (NeurIPS), 2022 |
 The Isabelle ENIGMAInternational Conference on Interactive Theorem Proving (ITP), 2022 |
 Learning to solve geometric construction problems from imagesInternational Conference on Intelligent Computer Mathematics (CICM), 2021 |
 The Role of Entropy in Guiding a Connection ProverInternational Conference on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX), 2021 |
 Online Machine Learning Techniques for Coq: A ComparisonInternational Conference on Intelligent Computer Mathematics (CICM), 2021 |
 TacticZero: Learning to Prove Theorems from Scratch with Deep
Reinforcement LearningNeural Information Processing Systems (NeurIPS), 2021 |
 Proof Artifact Co-training for Theorem Proving with Language ModelsInternational Conference on Learning Representations (ICLR), 2021 |
 LIME: Learning Inductive Bias for Primitives of Mathematical ReasoningInternational Conference on Machine Learning (ICML), 2021 |
 Faster Smarter Induction in Isabelle/HOLInternational Joint Conference on Artificial Intelligence (IJCAI), 2020 |
