AI Theorem Proving Papers

To start reading AI theorem proving papers, choose a proof environment and an evaluation question first. This selection covers premise retrieval in Lean, formal mathematics benchmarks, feedback-guided proof search, and higher-order logic. The four starting papers below were chosen to expose those differences; they are not a performance ranking or a complete survey of the latest systems.

Building a Lean-based prover? Start with LeanDojo (2023). Its toolkit extracts proof data and provides programmatic interaction with Lean; ReProver retrieves premises before generating tactics. The released benchmark contains 98,734 theorems and proofs. Pay attention to its novel-premises split: success on familiar library dependencies can hide a retrieval weakness that appears when a theorem needs premises unseen during training.

Comparing formal mathematics results? Read miniF2F (2021) before comparing model scores. It introduces 488 formalized problem statements drawn from competition and educational mathematics, with versions across proof assistants. A benchmark is an evaluation resource, not a prover. Check the exact assistant, validation/test split, available tactics and attempt budget before treating two reported percentages as comparable.

To study learning from proof-assistant feedback, read DeepSeek-Prover-V1.5 (2024). It combines supervised fine-tuning, reinforcement learning and Monte-Carlo tree search for Lean 4 proof generation. Use it to separate the learned model from the search procedure: a successful proof found after many attempts answers a different deployment question from a proof generated on the first attempt. Record both the search budget and the proof-checking environment when reproducing results.

For a contrasting environment, read HOList (2019). It exposes higher-order theorem proving in HOL Light as a machine-learning benchmark and interaction environment. This is useful when deciding which conclusions depend on Lean-specific tooling. A method demonstrated in HOL Light does not automatically establish the same result in Lean; libraries, proof states and available actions differ.

If your goal is a first reproducible experiment, our suggested order is miniF2F for the evaluation contract, LeanDojo for the retrieval and environment interface, then DeepSeek-Prover-V1.5 for feedback and search. Read HOList alongside these when comparing proof-assistant ecosystems. Each linked explanation includes the original paper so you can check the implementation and experimental conditions.

Before choosing a system, write down the proof assistant and version, training-data overlap, timeout, number of attempts, and whether the final proof is checked by the assistant. These are selection criteria rather than a universal leaderboard. A checked proof establishes the formal statement supplied to the assistant; it does not, by itself, establish that the statement captures the intended informal mathematics.