Autoformalization in the Era of Large Language Models: A Survey May 29, 2025 Automated Theorem Proving
Code Code Available DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition Apr 30, 2025 Automated Theorem Proving Large Language Model
Code Code Available Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Apr 18, 2024 Automated Theorem Proving Hallucination
Code Code Available DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search Aug 15, 2024 Automated Theorem Proving Language Modeling
Code Code Available Lean Workbook: A large-scale Lean problem set formalized from natural language math problems Jun 6, 2024 Automated Theorem Proving Math
Code Code Available miniCTX: Neural Theorem Proving with (Long-)Contexts Aug 5, 2024 Automated Theorem Proving
Code Code Available LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover Jul 24, 2024 Automated Theorem Proving Math
Code Code Available InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems Oct 21, 2024 Automated Theorem Proving CPU
Code Code Available A Survey on Deep Learning for Theorem Proving Apr 15, 2024 Automated Theorem Proving Deep Learning
Code Code Available Llemma: An Open Language Model For Mathematics Oct 16, 2023 Arithmetic Reasoning Automated Theorem Proving
Code Code Available Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving Feb 11, 2025 Automated Theorem Proving Large Language Model
Code Code Available PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition Jul 15, 2024 Automated Theorem Proving
Code Code Available Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning Apr 15, 2025 Automated Theorem Proving Large Language Model
Code Code Available An Empirical Study of Data Ability Boundary in LLMs' Math Reasoning Feb 23, 2024 Arithmetic Reasoning Automated Theorem Proving
Code Code Available LeanDojo: Theorem Proving with Retrieval-Augmented Language Models Jun 27, 2023 Automated Theorem Proving GPU
Code Code Available LeanAgent: Lifelong Learning for Formal Theorem Proving Oct 8, 2024 Abstract Algebra Automated Theorem Proving
Code Code Available Learning Formal Mathematics From Intrinsic Motivation Jun 30, 2024 Automated Theorem Proving Language Modeling
Code Code Available Formal Mathematics Statement Curriculum Learning Feb 3, 2022 Automated Theorem Proving Language Modeling
Code Code Available LeanExplore: A search engine for Lean 4 declarations Jun 4, 2025 Automated Theorem Proving
Code Code Available STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving Jan 31, 2025 Automated Theorem Proving
Code Code Available Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 Oct 21, 2024 Automated Theorem Proving
Code Code Available Parsel: Algorithmic Reasoning with Language Models by Composing Decompositions Dec 20, 2022 Automated Theorem Proving Code Generation
Code Code Available MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data Feb 14, 2024 Automated Theorem Proving Language Modelling
Code Code Available MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics Aug 31, 2021 Automated Theorem Proving
Code Code Available NaturalProofs: Mathematical Theorem Proving in Natural Language Mar 24, 2021 Automated Theorem Proving Domain Generalization
Code Code Available Lyra: Orchestrating Dual Correction in Automated Theorem Proving Sep 27, 2023 Automated Theorem Proving Hallucination
Code Code Available Logical Neural Networks Jun 23, 2020 Automated Theorem Proving Logical Reasoning
Code Code Available MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving Mar 5, 2025 Automated Theorem Proving Transfer Learning
Code Code Available Linear algebra with transformers Dec 3, 2021 Automated Theorem Proving Few-Shot Learning
Code Code Available LEGO-Prover: Neural Theorem Proving with Growing Libraries Oct 1, 2023 Automated Theorem Proving
Code Code Available Logical Inferences with Comparatives and Generalized Quantifiers May 16, 2020 Automated Theorem Proving Natural Language Inference
Code Code Available Measuring Systematic Generalization in Neural Proof Generation with Transformers Sep 30, 2020 Automated Theorem Proving Logical Reasoning
Code Code Available NaturalProver: Grounded Mathematical Proof Generation with Language Models May 25, 2022 Automated Theorem Proving Language Modeling
Code Code Available LeanReasoner: Boosting Complex Logical Reasoning with Lean Mar 20, 2024 Automated Theorem Proving Logical Reasoning
Code Code Available Learning as Abduction: Trainable Natural Logic Theorem Prover for Natural Language Inference Oct 29, 2020 Automated Theorem Proving Natural Language Inference
Code Code Available Leanabell-Prover: Posttraining Scaling in Formal Reasoning Apr 8, 2025 Automated Theorem Proving reinforcement-learning
Code Code Available AI Descartes: Combining Data and Theory for Derivable Scientific Discovery Sep 3, 2021 Automated Theorem Proving BIG-bench Machine Learning
Code Code Available INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving Jul 6, 2020 Automated Theorem Proving
Code Code Available Learning Theorem Proving Components Jul 21, 2021 Automated Theorem Proving Graph Neural Network
Code Code Available Beyond Autoregression: Fast LLMs via Self-Distillation Through Time Oct 28, 2024 Automated Theorem Proving Code Generation
Code Code Available FIMO: A Challenge Formal Dataset for Automated Theorem Proving Sep 8, 2023 Automated Theorem Proving
Code Code Available LangPro: Natural Language Theorem Prover Aug 30, 2017 Automated Theorem Proving Natural Language Inference
Code Code Available Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs Oct 21, 2022 Automated Theorem Proving Language Modeling
Code Code Available A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving Nov 5, 2019 Automated Theorem Proving Deep Reinforcement Learning
Code Code Available Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis Jan 30, 2025 Automated Theorem Proving Math
Code Code Available An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations May 15, 2023 Automated Theorem Proving Transfer Learning
Code Code Available An In-Context Learning Agent for Formal Theorem-Proving Oct 6, 2023 Automated Theorem Proving In-Context Learning
Code Code Available Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving May 25, 2023 Automated Theorem Proving
Code Code Available DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning May 29, 2025 Automated Theorem Proving Mathematical Reasoning
Code Code Available CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization Jul 8, 2025 Active Learning Automated Theorem Proving
Code Code Available 