README
Awesome-Formal-Mathematics
The official repo for “Toward Research-Level Formal Mathematics with Large Language Models”
📖 Table of Contents
- Awesome-Formal-Mathematics-Survey
📌 Overview
Recent developments in AI for Mathematics (AI4Math) — especially LLM-driven theorem provers — have achieved remarkable milestones in formal proof generation within Interactive Theorem Proving (ITP) environments such as Lean 4, Coq, and Isabelle. However, current systems remain fundamentally limited when tackling frontier research mathematics: discovering new theorems, resolving open conjectures, and engaging with problems that are open-ended, under-specified, and deeply abstract.
We argue that the next leap requires a decisive shift from predefined problem-solvers to research agents capable of addressing frontier mathematical challenges with rigorous formal reasoning. This repository organizes the literature covered in our position paper across:
- Autoformalization — translating natural language mathematics into ITP-verifiable formal statements
- Training Strategies — SFT, RL, expert iteration, and reflective learning for proof generation
- Test-time Adaptation — planning, decomposition, and retrieval augmentation at inference time
- Agentic Proving — multi-agent, tool-augmented proving systems
- Datasets & Benchmarks — evaluation infrastructure for neural theorem proving
🗂️ Taxonomy
We organize recent approaches along three complementary axes:
| Axis | Categories |
|---|---|
| Training Strategies (§3.1) | Supervised Fine-Tuning · Reinforcement Learning · Search-in-the-Loop · Reflective Learning |
| Test-time Adaptation (§3.2) | Planning & Decomposition · Theorem Retrieval · Search Algorithms |
| System Architecture (§3.3) | Generative Policy · Structural Search · Systematic Agent Prover |
Tag Legend:
| Tag | Meaning |
|---|---|
 | Supervised Fine-Tuning / Expert Iteration |
 | Reinforcement Learning |
 | Search-in-the-Loop (MCTS, BFS, expert iteration cycles) |
 | Planning / Subgoal Decomposition |
 | Premise / Theorem Retrieval |
 | Agentic / Multi-Agent Systems |
 | Autoformalization |
 | Dataset / Benchmark |
📑 Paper List
1. Autoformalization
Autoformalization bridges informal mathematics (natural language proofs, textbook statements) and formal ITP languages, addressing semantic ambiguity, type mismatch, and library alignment.
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Autoformalization with Large Language Models | | NeurIPS | 2022 | — |
| Thor: Wielding Hammers to Integrate LMs and ATPs | | NeurIPS | 2022 | — |
| Draft, Sketch, and Prove (DSP) | | ICLR (Oral) | 2023 |  |
| ProofNet: Autoformalizing Undergraduate-Level Math | | Preprint | 2023 |  |
| Herald: A Natural Language Annotated Lean 4 Dataset | | ICLR | 2025 |  |
| ATLAS: Autoformalizing via Lifting, Augmentation & Synthesis | | NeurIPS | 2025 |  |
| QDTSynth: Quality-Driven Theorem Synthesis | | ACL | 2025 | — |
| MASA: Multi-Agent Autoformalization | | EMNLP Demo | 2025 |  |
| LTRAG: Thought-Guided RAG for Autoformalization | | ACL Findings | 2025 |  |
| ReForm: Reflective Autoformalization with Bounded Seq Opt | | ICLR | 2026 |  |
| Autoformalization Survey (Weng et al.) | | Preprint | 2025 | — |
| A Lean Dataset for IMO: Small Steps for Hard Problems | | TMLR | 2025 |  |
2. Training Strategies
2.1 Supervised Fine-Tuning & Expert Iteration
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| GPT-f: Generative Language Modeling for ATP | | Preprint | 2020 |  |
| Proof Artifact Co-training (PACT) | | ICLR | 2022 | — |
| TheoremLlama: Transforming LLMs into Lean4 Experts | | EMNLP | 2024 |  |
| DeepSeek-Prover: Large-Scale Synthetic Data for ATP | | Preprint | 2024 | — |
| HunyuanProver: Scalable Data Synthesis & Guided Tree Search | | Preprint | 2024 | — |
| Goedel-Prover: Frontier Open-Source ATP | | Preprint | 2025 |  |
| Goedel-Prover-V2: Scaffolded Synthesis & Self-Correction | | Preprint | 2025 |  |
| Kimina-Prover: Large Formal Reasoning Models with RL | | Preprint | 2025 |  |
| DeepTheorem: LLM Reasoning via NL and RL | | Preprint | 2025 |  |
| SEED-Prover: Deep and Broad Reasoning for ATP | | Preprint | 2025 |  |
2.2 Reinforcement Learning
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| DeepSeek-Prover-V1.5: RLPAF + MCTS | | ICLR | 2025 |  |
| AlphaProof: RL for Formal Math (IMO Silver Medal) | | Blog | 2024 | — |
| AlphaProof (Nature): Olympiad-level RL Proving | | Nature | 2025 | — |
| Abel: Sample Efficient Online RL for ATP | | NeurIPS-W | 2024 | — |
| DeepSeek-Prover-V2: RL for Subgoal Decomposition | | Preprint | 2025 |  |
| Leanabell-Prover: Posttraining Scaling in Formal Reasoning | | Preprint | 2025 |  |
| Leanabell-Prover-V2: Verifier-Integrated RL | | Preprint | 2025 |  |
| Scaling Multi-Turn Off-Policy RL & Multi-Agent Tree Search | | Preprint | 2025 | — |
| Seed-Prover 1.5: Agentic RL for Theorem Proving | | Preprint | 2025 | |
| GAR: Generative Adversarial RL for Formal ATP | | Preprint | 2025 | — |
2.3 Search-in-the-Loop Training
Expert iteration with proof search (MCTS, BFS, etc.) embedded in the training loop, iteratively bootstrapping stronger provers.
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Deep Network Guided Proof Search (E-prover) | | LPAR | 2017 | — |
| HyperTree Proof Search (HTPS) | | NeurIPS | 2022 | — |
| InternLM2.5-StepProver: Expert Iteration on Large-Scale Lean | | Preprint | 2024 |  |
| BFS-Prover: Best-First Tree Search for LLM ATP | | ACL | 2025 | — |
| MPS-Prover: Multi-Perspective Search & Data Curation | | Preprint | 2025 | — |
| STP: Self-play Theorem Proving via Iterative Conjecturing | | Preprint | 2025 |  |
2.4 Reflective Learning
Learning from failure: verifier feedback, self-correction, and subgoal decomposition rewards.
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Baldur: Whole-Proof Generation and Repair | | ESEC/FSE | 2023 | — |
| Decomposing the Enigma: Subgoal-Based Demo Learning | | Preprint | 2023 |  |
| POETRY: Proving Theorems Recursively | | NeurIPS | 2024 |  |
| SubgoalXL: Subgoal-Based Expert Learning | | Preprint | 2024 |  |
| Lyra: Orchestrating Dual Correction in ATP | | TMLR | 2024 |  |
| Hierarchical Proof Decomposition via Rewarding LLMs | | Preprint | 2024 | — |
| HybridProver: LLM-Driven Proof Synthesis & Refinement | | Preprint | 2025 | — |
| Decomposition-Based Solving with Iterative Reflection | | Preprint | 2025 | — |
3. Test-time Adaptation
3.1 Planning & Theorem Decomposition
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Draft, Sketch, and Prove (DSP) | | ICLR (Oral) | 2023 | |
| DeepSeek-Prover-V2: Subgoal Decomposition | | Preprint | 2025 | |
| Reviving DSP for Advanced Theorem Proving | | Preprint | 2025 |  |
| Hilbert: Recursive Decomposition + RAG (99.2% MiniF2F) | | Preprint | 2025 | — |
| StepFun-Prover: Think and Verify Step by Step | | Preprint | 2025 |  |
| ProofCompass: Guiding Formal Proof Search with LLMs | | ICML-W | 2025 | — |
| DeepTheorem: NL → Formal via Informal Planning | | Preprint | 2025 | |
| PaCoRe: Parallel Coordinated Reasoning | | Preprint | 2026 |  |
3.2 Theorem Retrieval
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| LeanDojo / ReProver: Retrieval-Augmented LLMs for Lean | | NeurIPS (Oral) | 2023 |  |
| COPRA: In-Context Learning for Theorem Proving | | COLM | 2024 |  |
| LEGO-Prover: Dynamic Growing Proof Library | | ICLR | 2024 |  |
| LeanAgent: Lifelong Learning for Formal Theorem Proving | | ICLR | 2025 |  |
| LemmaHead: RAG-Assisted Proof Generation | | Preprint | 2025 | — |
| ProofNet++: Neuro-Symbolic Verification with Self-Correction | | Preprint | 2025 | — |
4. Systematic Agent Prover
LLMs as autonomous agents: multi-step planning, tool use (ITP interaction, library retrieval, code execution), reflection, and multi-agent collaboration.
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Proving Olympiad Algebraic Inequalities without Human Demos | | NeurIPS | 2024 | — |
| Proving Olympiad Inequalities by LLMs + Symbolic Reasoning | | ICLR | 2025 |  |
| APOLLO: Automated LLM and Lean Collaboration | | Preprint | 2025 | — |
| Prover Agent: Agent-Based Framework for Formal Proofs | | ICML-W | 2025 |  |
| Seed-Prover 1.5: Agentic RL + Tool Use | | Preprint | 2025 | |
| MASA: Multi-Agent System for Autoformalization | | EMNLP Demo | 2025 | |
| Aristotle: IMO-level ATP | | Preprint | 2025 | — |
| Advancing Mathematical Research via Human-AI Interactive TP | | Preprint | 2025 | — |
5. Foundation Models for Math
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| GPT-f: Generative Language Modeling for ATP | | Preprint | 2020 | |
| LLEMMA: Open Language Model for Mathematics | | ICLR | 2024 |  |
| DeepSeekMath: Pushing the Limits of Math Reasoning | | Preprint | 2024 |  |
| OpenAI o1: Learning to Reason | | Preprint | 2024 | — |
| DeepSeek-R1: Incentivizing Reasoning via RL | | Preprint | 2025 | — |
| Gemini 2.5: Advanced Reasoning & Agentic Capabilities | | Preprint | 2025 | — |
6. Datasets & Benchmarks
| Dataset / Benchmark | ITP | Scale | Venue | Year | Code |
|---|---|---|---|---|---|
| CoqGym | Coq | 71K proofs, 123 projects | ICML | 2019 |  |
| HOList | HOL Light | 29K theorems | ICML | 2019 | — |
| MATH | — | 12.5K problems | NeurIPS D&B | 2021 |  |
| miniF2F | Lean / Isabelle / Coq | 488 Olympiad problems | ICLR | 2022 |  |
| ProofNet | Lean | 371 undergrad problems | Preprint | 2023 | |
| LeanDojo (Mathlib) | Lean 4 | 140M+ tokens | NeurIPS (Oral) | 2023 | |
| Lean Workbook | Lean 4 | 57K problems | Preprint | 2024 | |
| PutnamBench | Lean / Isabelle / Coq | 1697 competition problems | NeurIPS D&B | 2024 |  |
| Herald | Lean 4 | NL-annotated Lean | ICLR | 2025 | |
| FrontierMath | — | Research-level | Preprint | 2024 | — |
| CombiBench | Lean 4 | Combinatorics | Preprint | 2025 |  |
| FATE | Lean 4 | Algebra | Preprint | 2025 | — |
| IneqMath | Lean 4 | Inequalities | NeurIPS Spotlight | 2025 |  |
| FormalMath | Lean 4 | 5.6K problems | Preprint | 2025 | — |
| IMO Lean Dataset | Lean 4 | IMO problems | TMLR | 2025 | |
| ProverBench | Lean 4 | Textbook | Preprint | 2025 | — |
| Formal Conjectures | Lean 4 | Open conjectures | — | 2026 |  |
7. Interactive Theorem Provers & Tools
| System | Foundation | Key Features | ML Ecosystem | Code |
|---|---|---|---|---|
| Lean 4 | CIC (Dependent Type Theory) | Mathlib (1.9M+ LOC), active community | LeanDojo, TheoremLlama, extensive |  |
| Mathlib4 | Lean 4 library | 1.9M+ LOC, 140K+ theorems | Core of most Lean provers |  |
| Coq (Rocq) | CIC | 383K+ declarations, CompCert, Four Color Theorem | CoqGym | — |
| Isabelle/HOL | HOL | Sledgehammer automation, AFP (5M+ LOC) | LISA, IsarStep | — |
| HOL Light | HOL | Kepler Conjecture formalization | HOList | — |
| Metamath | ZFC Set Theory | Minimalist, 40K+ theorems | GPT-f origin | — |
| AlphaGeometry | Geometry-specific | Neural + algebraic, deductive database | Built-in | — |
🔮 Open Challenges
We identify five critical open challenges for advancing toward research-level formal mathematics:
| # | Challenge | Description |
|---|---|---|
| 1 | Data Scarcity & Evaluation | Formal math corpora remain orders of magnitude smaller than informal ones; specification fidelity and benchmark contamination are growing concerns |
| 2 | Relational Structure | Current provers treat theorems in isolation; mathematical research requires understanding deep structural relationships between concepts |
| 3 | Discovery vs. Verification | Existing systems verify known results but cannot discover new theorems, conjecture, or engage in exploratory reasoning |
| 4 | Tool Ecosystem | Proof assistants need tighter integration with computational tools (CAS, numerical solvers, visualization) |
| 5 | Human–AI Collaboration | Smooth interactive workflows for mathematician–AI collaboration require uncertainty estimation, calibrated confidence, and intuitive interfaces |
Contributors
ericjiang18
3 commits
Similar repos
README
Awesome-Formal-Mathematics
The official repo for “Toward Research-Level Formal Mathematics with Large Language Models”
📖 Table of Contents
- Awesome-Formal-Mathematics-Survey
📌 Overview
Recent developments in AI for Mathematics (AI4Math) — especially LLM-driven theorem provers — have achieved remarkable milestones in formal proof generation within Interactive Theorem Proving (ITP) environments such as Lean 4, Coq, and Isabelle. However, current systems remain fundamentally limited when tackling frontier research mathematics: discovering new theorems, resolving open conjectures, and engaging with problems that are open-ended, under-specified, and deeply abstract.
We argue that the next leap requires a decisive shift from predefined problem-solvers to research agents capable of addressing frontier mathematical challenges with rigorous formal reasoning. This repository organizes the literature covered in our position paper across:
- Autoformalization — translating natural language mathematics into ITP-verifiable formal statements
- Training Strategies — SFT, RL, expert iteration, and reflective learning for proof generation
- Test-time Adaptation — planning, decomposition, and retrieval augmentation at inference time
- Agentic Proving — multi-agent, tool-augmented proving systems
- Datasets & Benchmarks — evaluation infrastructure for neural theorem proving
🗂️ Taxonomy
We organize recent approaches along three complementary axes:
| Axis | Categories |
|---|---|
| Training Strategies (§3.1) | Supervised Fine-Tuning · Reinforcement Learning · Search-in-the-Loop · Reflective Learning |
| Test-time Adaptation (§3.2) | Planning & Decomposition · Theorem Retrieval · Search Algorithms |
| System Architecture (§3.3) | Generative Policy · Structural Search · Systematic Agent Prover |
Tag Legend:
| Tag | Meaning |
|---|---|
| Supervised Fine-Tuning / Expert Iteration |
| Reinforcement Learning |
| Search-in-the-Loop (MCTS, BFS, expert iteration cycles) |
| Planning / Subgoal Decomposition |
| Premise / Theorem Retrieval |
| Agentic / Multi-Agent Systems |
| Autoformalization |
| Dataset / Benchmark |
📑 Paper List
1. Autoformalization
Autoformalization bridges informal mathematics (natural language proofs, textbook statements) and formal ITP languages, addressing semantic ambiguity, type mismatch, and library alignment.
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Autoformalization with Large Language Models | | NeurIPS | 2022 | — |
| Thor: Wielding Hammers to Integrate LMs and ATPs | | NeurIPS | 2022 | — |
| Draft, Sketch, and Prove (DSP) | | ICLR (Oral) | 2023 | |
| ProofNet: Autoformalizing Undergraduate-Level Math | | Preprint | 2023 | |
| Herald: A Natural Language Annotated Lean 4 Dataset | | ICLR | 2025 | |
| ATLAS: Autoformalizing via Lifting, Augmentation & Synthesis | | NeurIPS | 2025 | |
| QDTSynth: Quality-Driven Theorem Synthesis | | ACL | 2025 | — |
| MASA: Multi-Agent Autoformalization | | EMNLP Demo | 2025 | |
| LTRAG: Thought-Guided RAG for Autoformalization | | ACL Findings | 2025 | |
| ReForm: Reflective Autoformalization with Bounded Seq Opt | | ICLR | 2026 | |
| Autoformalization Survey (Weng et al.) | | Preprint | 2025 | — |
| A Lean Dataset for IMO: Small Steps for Hard Problems | | TMLR | 2025 | |
2. Training Strategies
2.1 Supervised Fine-Tuning & Expert Iteration
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| GPT-f: Generative Language Modeling for ATP | | Preprint | 2020 | |
| Proof Artifact Co-training (PACT) | | ICLR | 2022 | — |
| TheoremLlama: Transforming LLMs into Lean4 Experts | | EMNLP | 2024 | |
| DeepSeek-Prover: Large-Scale Synthetic Data for ATP | | Preprint | 2024 | — |
| HunyuanProver: Scalable Data Synthesis & Guided Tree Search | | Preprint | 2024 | — |
| Goedel-Prover: Frontier Open-Source ATP | | Preprint | 2025 | |
| Goedel-Prover-V2: Scaffolded Synthesis & Self-Correction | | Preprint | 2025 | |
| Kimina-Prover: Large Formal Reasoning Models with RL | | Preprint | 2025 | |
| DeepTheorem: LLM Reasoning via NL and RL | | Preprint | 2025 | |
| SEED-Prover: Deep and Broad Reasoning for ATP | | Preprint | 2025 | |
2.2 Reinforcement Learning
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| DeepSeek-Prover-V1.5: RLPAF + MCTS | | ICLR | 2025 | |
| AlphaProof: RL for Formal Math (IMO Silver Medal) | | Blog | 2024 | — |
| AlphaProof (Nature): Olympiad-level RL Proving | | Nature | 2025 | — |
| Abel: Sample Efficient Online RL for ATP | | NeurIPS-W | 2024 | — |
| DeepSeek-Prover-V2: RL for Subgoal Decomposition | | Preprint | 2025 | |
| Leanabell-Prover: Posttraining Scaling in Formal Reasoning | | Preprint | 2025 | |
| Leanabell-Prover-V2: Verifier-Integrated RL | | Preprint | 2025 | |
| Scaling Multi-Turn Off-Policy RL & Multi-Agent Tree Search | | Preprint | 2025 | — |
| Seed-Prover 1.5: Agentic RL for Theorem Proving | | Preprint | 2025 | |
| GAR: Generative Adversarial RL for Formal ATP | | Preprint | 2025 | — |
2.3 Search-in-the-Loop Training
Expert iteration with proof search (MCTS, BFS, etc.) embedded in the training loop, iteratively bootstrapping stronger provers.
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Deep Network Guided Proof Search (E-prover) | | LPAR | 2017 | — |
| HyperTree Proof Search (HTPS) | | NeurIPS | 2022 | — |
| InternLM2.5-StepProver: Expert Iteration on Large-Scale Lean | | Preprint | 2024 | |
| BFS-Prover: Best-First Tree Search for LLM ATP | | ACL | 2025 | — |
| MPS-Prover: Multi-Perspective Search & Data Curation | | Preprint | 2025 | — |
| STP: Self-play Theorem Proving via Iterative Conjecturing | | Preprint | 2025 | |
2.4 Reflective Learning
Learning from failure: verifier feedback, self-correction, and subgoal decomposition rewards.
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Baldur: Whole-Proof Generation and Repair | | ESEC/FSE | 2023 | — |
| Decomposing the Enigma: Subgoal-Based Demo Learning | | Preprint | 2023 | |
| POETRY: Proving Theorems Recursively | | NeurIPS | 2024 | |
| SubgoalXL: Subgoal-Based Expert Learning | | Preprint | 2024 | |
| Lyra: Orchestrating Dual Correction in ATP | | TMLR | 2024 | |
| Hierarchical Proof Decomposition via Rewarding LLMs | | Preprint | 2024 | — |
| HybridProver: LLM-Driven Proof Synthesis & Refinement | | Preprint | 2025 | — |
| Decomposition-Based Solving with Iterative Reflection | | Preprint | 2025 | — |
3. Test-time Adaptation
3.1 Planning & Theorem Decomposition
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Draft, Sketch, and Prove (DSP) | | ICLR (Oral) | 2023 | |
| DeepSeek-Prover-V2: Subgoal Decomposition | | Preprint | 2025 | |
| Reviving DSP for Advanced Theorem Proving | | Preprint | 2025 | |
| Hilbert: Recursive Decomposition + RAG (99.2% MiniF2F) | | Preprint | 2025 | — |
| StepFun-Prover: Think and Verify Step by Step | | Preprint | 2025 | |
| ProofCompass: Guiding Formal Proof Search with LLMs | | ICML-W | 2025 | — |
| DeepTheorem: NL → Formal via Informal Planning | | Preprint | 2025 | |
| PaCoRe: Parallel Coordinated Reasoning | | Preprint | 2026 | |
3.2 Theorem Retrieval
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| LeanDojo / ReProver: Retrieval-Augmented LLMs for Lean | | NeurIPS (Oral) | 2023 | |
| COPRA: In-Context Learning for Theorem Proving | | COLM | 2024 | |
| LEGO-Prover: Dynamic Growing Proof Library | | ICLR | 2024 | |
| LeanAgent: Lifelong Learning for Formal Theorem Proving | | ICLR | 2025 | |
| LemmaHead: RAG-Assisted Proof Generation | | Preprint | 2025 | — |
| ProofNet++: Neuro-Symbolic Verification with Self-Correction | | Preprint | 2025 | — |
4. Systematic Agent Prover
LLMs as autonomous agents: multi-step planning, tool use (ITP interaction, library retrieval, code execution), reflection, and multi-agent collaboration.
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| Proving Olympiad Algebraic Inequalities without Human Demos | | NeurIPS | 2024 | — |
| Proving Olympiad Inequalities by LLMs + Symbolic Reasoning | | ICLR | 2025 | |
| APOLLO: Automated LLM and Lean Collaboration | | Preprint | 2025 | — |
| Prover Agent: Agent-Based Framework for Formal Proofs | | ICML-W | 2025 | |
| Seed-Prover 1.5: Agentic RL + Tool Use | | Preprint | 2025 | |
| MASA: Multi-Agent System for Autoformalization | | EMNLP Demo | 2025 | |
| Aristotle: IMO-level ATP | | Preprint | 2025 | — |
| Advancing Mathematical Research via Human-AI Interactive TP | | Preprint | 2025 | — |
5. Foundation Models for Math
| Paper | Tags | Venue | Year | Code |
|---|---|---|---|---|
| GPT-f: Generative Language Modeling for ATP | | Preprint | 2020 | |
| LLEMMA: Open Language Model for Mathematics | | ICLR | 2024 | |
| DeepSeekMath: Pushing the Limits of Math Reasoning | | Preprint | 2024 | |
| OpenAI o1: Learning to Reason | | Preprint | 2024 | — |
| DeepSeek-R1: Incentivizing Reasoning via RL | | Preprint | 2025 | — |
| Gemini 2.5: Advanced Reasoning & Agentic Capabilities | | Preprint | 2025 | — |
6. Datasets & Benchmarks
| Dataset / Benchmark | ITP | Scale | Venue | Year | Code |
|---|---|---|---|---|---|
| CoqGym | Coq | 71K proofs, 123 projects | ICML | 2019 | |
| HOList | HOL Light | 29K theorems | ICML | 2019 | — |
| MATH | — | 12.5K problems | NeurIPS D&B | 2021 | |
| miniF2F | Lean / Isabelle / Coq | 488 Olympiad problems | ICLR | 2022 | |
| ProofNet | Lean | 371 undergrad problems | Preprint | 2023 | |
| LeanDojo (Mathlib) | Lean 4 | 140M+ tokens | NeurIPS (Oral) | 2023 | |
| Lean Workbook | Lean 4 | 57K problems | Preprint | 2024 | |
| PutnamBench | Lean / Isabelle / Coq | 1697 competition problems | NeurIPS D&B | 2024 | |
| Herald | Lean 4 | NL-annotated Lean | ICLR | 2025 | |
| FrontierMath | — | Research-level | Preprint | 2024 | — |
| CombiBench | Lean 4 | Combinatorics | Preprint | 2025 | |
| FATE | Lean 4 | Algebra | Preprint | 2025 | — |
| IneqMath | Lean 4 | Inequalities | NeurIPS Spotlight | 2025 | |
| FormalMath | Lean 4 | 5.6K problems | Preprint | 2025 | — |
| IMO Lean Dataset | Lean 4 | IMO problems | TMLR | 2025 | |
| ProverBench | Lean 4 | Textbook | Preprint | 2025 | — |
| Formal Conjectures | Lean 4 | Open conjectures | — | 2026 | |
7. Interactive Theorem Provers & Tools
| System | Foundation | Key Features | ML Ecosystem | Code |
|---|---|---|---|---|
| Lean 4 | CIC (Dependent Type Theory) | Mathlib (1.9M+ LOC), active community | LeanDojo, TheoremLlama, extensive | |
| Mathlib4 | Lean 4 library | 1.9M+ LOC, 140K+ theorems | Core of most Lean provers | |
| Coq (Rocq) | CIC | 383K+ declarations, CompCert, Four Color Theorem | CoqGym | — |
| Isabelle/HOL | HOL | Sledgehammer automation, AFP (5M+ LOC) | LISA, IsarStep | — |
| HOL Light | HOL | Kepler Conjecture formalization | HOList | — |
| Metamath | ZFC Set Theory | Minimalist, 40K+ theorems | GPT-f origin | — |
| AlphaGeometry | Geometry-specific | Neural + algebraic, deductive database | Built-in | — |
🔮 Open Challenges
We identify five critical open challenges for advancing toward research-level formal mathematics:
| # | Challenge | Description |
|---|---|---|
| 1 | Data Scarcity & Evaluation | Formal math corpora remain orders of magnitude smaller than informal ones; specification fidelity and benchmark contamination are growing concerns |
| 2 | Relational Structure | Current provers treat theorems in isolation; mathematical research requires understanding deep structural relationships between concepts |
| 3 | Discovery vs. Verification | Existing systems verify known results but cannot discover new theorems, conjecture, or engage in exploratory reasoning |
| 4 | Tool Ecosystem | Proof assistants need tighter integration with computational tools (CAS, numerical solvers, visualization) |
| 5 | Human–AI Collaboration | Smooth interactive workflows for mathematician–AI collaboration require uncertainty estimation, calibrated confidence, and intuitive interfaces |
Similar repos
Contributors
ericjiang18
3 commits