# Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs

arXiv: https://arxiv.org/abs/2503.04772 · HTML: https://mlsanity.com/paper/2503.04772/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 26 references that are in the map.
- First posted on arXiv 16 Feb 2025.

## Builds on (most cited first, 12 of 12)

- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [A Simple Framework for Contrastive Learning of Visual Representations](https://mlsanity.com/paper/2002.05709/) (2020)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [Scaling Instruction-Finetuned Language Models](https://mlsanity.com/paper/2210.11416/) (2022)
- [ByT5: Towards a token-free future with pre-trained byte-to-byte models](https://mlsanity.com/paper/2105.13626/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [The Faiss library](https://mlsanity.com/paper/2401.08281/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)

## Built on by (most cited first, 3 of 3)

- [Learning to Disprove: Formal Counterexample Generation with Large Language Models](https://mlsanity.com/paper/2603.19514/) (2026)
- [Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem](https://mlsanity.com/paper/2509.06809/) (2025)
- [TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics](https://mlsanity.com/paper/2606.09450/) (2026)

## Abstract (arXiv)

Large Language Models (LLMs) have demonstrated significant potential in generating mathematical proofs. However, a persistent challenge is that LLMs occasionally make mistakes, while even a minor mistake can invalidate an entire proof. Proof assistants like Lean offer a great remedy. They are designed for verifying each step of a proof in a formal language, and in recent years researchers have created AI models to generate proofs in their languages. However, the scarcity of large-scale datasets of Lean proofs restrict the performance of such Automated Theorem Proving (ATP) models. We developed LeanNavigator, a novel method for generating a large-scale dataset of Lean theorems and proofs by finding new ways to prove existing Lean theorems. By leveraging an interactive Lean client and an efficient method for proof step generation, LeanNavigator efficiently produces new theorems with corresponding proofs. Applying this approach to Mathlib4, we generated 4.7 million theorems totaling 1 billion tokens, surpassing previous datasets by more than an order of magnitude. Using this extensive dataset, we trained an AI model that outperforms the state-of-the-art ReProver model in theorem-proving tasks. These results confirm our hypothesis and demonstrate the critical role of large datasets in improving the performance of automated theorem provers.