Awesome-Formal-Mathematics

The official repo for “Toward Research-Level Formal Mathematics with Large Language Models”

📖 Table of Contents

• Awesome-Formal-Mathematics-Survey
  • 📖 Table of Contents
  • 📌 Overview
  • 🗂️ Taxonomy
  • 📑 Paper List
    • 1. Autoformalization
    • 2. Training Strategies
      • 2.1 Supervised Fine-Tuning & Expert Iteration
      • 2.2 Reinforcement Learning
      • 2.3 Search-in-the-Loop Training
      • 2.4 Reflective Learning
    • 3. Test-time Adaptation
      • 3.1 Planning & Theorem Decomposition
      • 3.2 Theorem Retrieval
    • 4. Systematic Agent Prover
    • 5. Foundation Models for Math
    • 6. Datasets & Benchmarks
    • 7. Interactive Theorem Provers & Tools
  • 🔮 Open Challenges

---

📌 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