A curated list of recent advancements in formal reasoning AI, including but not limited to papers and datasets about autoformalization, (semi-)automated theorem proving, code verification, and so on.
Currently work in progress. Please feel free to contribute!
This work is licensed under CC BY 4.0.
| Time | Name | Language | Links |
|---|---|---|---|
| 2025.04 | DeepSeek-Prover-V2 | Lean 4 | [HuggingFace] [Paper] |
| 2025.04 | Kimina-Prover Preview | Lean 4 | [HuggingFace] [Paper] |
| 2025.02 | Goedel-Prover | Lean 4 | [HuggingFace] [Paper] |
| 2025.02 | STP | Lean 4 | [HuggingFace] [Paper] |
| 2024.10 | InternLM2.5-Step-Prover | Lean 4 | [HuggingFace] [Paper] |
| 2024.08 | DeepSeek-Prover-V1.5 | Lean 4 | [HuggingFace] [Paper] |
| 2023.06 | ReProver | Lean 4 | [GitHub] [Paper] |
| Time | Name | Language | Links |
|---|---|---|---|
| 2025.04 | Kimina-Autoformalizer-7B | Lean 4 | [HuggingFace] [Paper] |
| Time | Name | Language | Links |
|---|---|---|---|
| 2024.10 | Herald: A Natural Language Annotated Lean 4 Dataset | Lean 4 | [HuggingFace] [Paper] |
| Time | Name | Language | Links |
|---|---|---|---|
| 2024.04 | LLMLean | Lean 4 | [GitHub] |
| 2023.12 | Lean Copilot | Lean 4 | [GitHub] [Paper] |
NL indicates problem statements in natural language.
| Time | Name | Language | Proof | Size | Links |
|---|---|---|---|---|---|
| 2025.02 | STP | Lean 4 | ✅ | 1.7M | [HuggingFace] [Paper] |
| 2024.07 | Lean-Github | Lean 4 | ✅ | 29k | [HuggingFace] [Paper] |
| 2024.06 | Lean-Workbook | NL, Lean 4 | 🟨 | 140k | [HuggingFace] [Paper] |
| 2023.06 | LeanDojo | Lean 3 & 4 | ✅ | 122k | [Lean 3] [Lean 4] [Paper] |
Italics indicates that some problems are unavailable in this language. Asterisk indicates that this language is provided by the community.
| Time | Name | Language | Size | Links |
|---|---|---|---|---|
| 2024.07 | ProverBench | NL, Lean 4 | 325 | [HuggingFace] [Paper] |
| 2024.07 | PutnamBench | NL, Lean 4, Isabelle, Coq | 657 | [Website] [GitHub] [Paper] |
| 2023.02 | ProofNet | NL, Lean 3 & 4* | 371 | [GitHub] [Lean4 ver.] [Paper] |
| 2021.09 | MiniF2F | NL*, Lean 3 & 4*, Metamath, Isabelle, Hol Light | 488 | [GitHub] [NL ver.] [Lean4 ver.] [Paper] |
This category only includes papers not mentioned in the above lists.
| Time | Name | Links |
|---|---|---|
| 2025.03 | Automated Discovery of Tactic Libraries for Interactive Theorem Proving | [Paper] |
| 2024.12 | Formal Mathematical Reasoning: A New Frontier in AI | [Paper] |
| 2024.07 | Learning Formal Mathematics From Intrinsic Motivation | [Paper] |
| 2023.10 | LEGO-Prover: Neural Theorem Proving with Growing Libraries | [Paper] |
| 2022.10 | Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs | [Paper] |