Automated Theorem Proving

Description from the archive archive 2025-07-28.

Benchmarks archive 2025-07-28

9 leaderboard tables shown for this task, 9 with rows (a “benchmark” on this site is a table with at least one row, as on /sota), ordered by row count. “Best model” is the first row in the archive's own order at snapshot; nothing is re-ranked here and metric direction is not recorded in the archive. PwC's Trend sparklines are not in the archive, so that column is omitted.

Syntology column: samples harvested from the paper's repositories and executed on synthesized fixtures; “ran” is not a correctness claim and does not order the table. A dash means no Syntology record for that paper, not a recorded non-run. Read from the graph 2026-09-24.

Libraries

Not in the archive: the export carries no per-task library table, so there is nothing to show at snapshot 2025-07-28.

Datasets archive 2025-07-28

8 datasets whose archive record lists this task, ordered by the archive's paper count.

Subtasks archive 2025-07-28

No subtask under this task in the archive's task tree.

Parent tasks archive 2025-07-28

Most implemented papers archive 2025-07-28

30 shown of 110 papers with code (288 tagged with this task in all), ordered by repositories listed in the archive, not by stars (the archive holds no stars, so PwC's “Social” and “Latest” sorts cannot be reproduced). Papers without a page here are shown as plain text.

• miniCTX: Neural Theorem Proving with (Long-)Contexts
  5 Aug 2024 4 repositories listed Syntology ran 5 of 5 samples · 0 unverified · 5 pointer-only (licence)
  We introduce miniCTX, which tests a model's ability to prove formal mathematical theorems that depend on new context that is not seen during training.
• Llemma: An Open Language Model For Mathematics
  16 Oct 2023 4 repositories listed Syntology ran 6 of 8 samples · 2 unverified
  We present Llemma, a large language model for mathematics.
• MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
  31 Aug 2021 4 repositories listed Syntology ran 3 of 3 samples · 0 unverified
  We present miniF2F, a dataset of formal Olympiad-level mathematics problems statements intended to provide a unified cross-system benchmark for neural theorem proving.
• Proof Artifact Co-training for Theorem Proving with Language Models
  11 Feb 2021 4 repositories listed Syntology ran 3 of 4 samples · 1 unverified
  Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built.
• Holophrasm: a neural Automated Theorem Prover for higher-order logic
  8 Aug 2016 4 repositories listed Syntology ran 0 of 14 samples · 14 unverified
  I propose a system for Automated Theorem Proving in higher order logic using deep learning and eschewing hand-constructed features.
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
  27 Jun 2023 3 repositories listed Syntology ran 1 of 9 samples · 8 unverified
  Using this data, we develop ReProver (Retrieval-Augmented Prover): an LLM-based prover augmented with retrieval for selecting premises from a vast math library.
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
  21 Oct 2022 3 repositories listed
  In this work, we introduce Draft, Sketch, and Prove (DSP), a method that maps informal proofs to formal proof sketches, and uses the sketches to guide an automated prover by directing its search to easier sub-problems.
• HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  5 Apr 2019 3 repositories listed
  We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic.
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
  29 May 2025 2 repositories listed Syntology ran 1 of 1 samples · 0 unverified · 1 pointer-only (licence)
  In this work, we propose DeepTheorem, a comprehensive informal theorem-proving framework exploiting natural language to enhance LLM mathematical reasoning.
• Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
  15 Apr 2025 2 repositories listed Syntology ran 3 of 3 samples · 0 unverified · 3 pointer-only (licence)
  We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview release.
• ProofWala: Multilingual Proof Data Synthesis and Theorem-Proving
  7 Feb 2025 2 repositories listed Syntology ran 0 of 11 samples · 11 unverified
  We address this weakness with a multilingual proof framework, PROOFWALA, that allows a standardized form of interaction between neural theorem-provers and two established ITPs (Coq and Lean).
• Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
  21 Oct 2024 2 repositories listed Syntology ran 0 of 2 samples · 2 unverified
  Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems.
• DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
  15 Aug 2024 2 repositories listed Syntology ran 4 of 10 samples · 6 unverified
  We introduce DeepSeek-Prover-V1.
• PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
  15 Jul 2024 2 repositories listed Syntology ran 3 of 3 samples · 0 unverified · 3 pointer-only (licence)
  We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems.
• Learning Formal Mathematics From Intrinsic Motivation
  30 Jun 2024 2 repositories listed Syntology ran 6 of 12 samples · 6 unverified
  We propose novel methods for hindsight relabeling on proof search trees to significantly improve the agent's sample efficiency in both tasks.
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
  18 Apr 2024 2 repositories listed Syntology ran 3 of 3 samples · 0 unverified
  Neural theorem proving combines large language models (LLMs) with proof assistants such as Lean, where the correctness of formal proofs can be rigorously verified, leaving no room for hallucination.
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
  24 Feb 2023 2 repositories listed Syntology ran 2 of 3 samples · 1 unverified
  We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics.
• Linear algebra with transformers
  3 Dec 2021 2 repositories listed
  Transformers can learn to perform numerical computations from examples only.
• Learning Symbolic Rules for Reasoning in Quasi-Natural Language
  23 Nov 2021 2 repositories listed
  In this work, we ask how we can build a rule-based system that can reason with natural language input but without the manual construction of rules.
• Learning to Match Mathematical Statements with Proofs
  3 Feb 2021 2 repositories listed
  The task is designed to improve the processing of research-level mathematical texts.
• Measuring Systematic Generalization in Neural Proof Generation with Transformers
  30 Sep 2020 2 repositories listed Syntology ran 1 of 1 samples · 0 unverified
  We observe that models that are not trained to generate proofs are better at generalizing to problems based on longer proofs.
• Logical Neural Networks
  23 Jun 2020 2 repositories listed Syntology ran 2 of 15 samples · 13 unverified
  We propose a novel framework seamlessly providing key properties of both neural nets (learning) and symbolic logic (knowledge and reasoning).
• Learning to Prove Theorems by Learning to Generate Theorems
  17 Feb 2020 2 repositories listed Syntology ran 0 of 11 samples · 11 unverified
  We consider the task of automated theorem proving, a key AI task.
• DeepMath - Deep Sequence Models for Premise Selection
  14 Jun 2016 2 repositories listed
  We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics.
• CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
  8 Jul 2025 1 repository listed
  Translating natural language mathematical statements into formal, executable code is a fundamental challenge in automated theorem proving.
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification
  5 Jun 2025 1 repository listed
  We propose a retrospective, step-aware formal verification framework Safe.
• LeanExplore: A search engine for Lean 4 declarations
  4 Jun 2025 1 repository listed Syntology ran 0 of 3 samples · 3 unverified
  This paper introduces LeanExplore, a search engine for Lean 4 declarations.
• Autoformalization in the Era of Large Language Models: A Survey
  29 May 2025 1 repository listed
  Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of…
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions
  24 May 2025 1 repository listed
  We present ConstructiveBench, a dataset of 3, 431 answer-construction problems in various math competitions with verified Lean formalizations.
• MIRB: Mathematical Information Retrieval Benchmark
  21 May 2025 1 repository listed
  In this paper, we introduce MIRB (Mathematical Information Retrieval Benchmark) to assess the MIR capabilities of retrieval models.

Syntology lines on 19 of the papers shown; no Syntology record for the others (a paper without an arXiv id cannot be joined to the graph, and absence from the graph layer is not a recorded non-run). “Ran” means the sample executed on a synthesized fixture, not that the paper's result was reproduced. Read from the graph 2026-09-24.