# Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 9 of its 21 references that are in the map.
- First posted on arXiv 8 Sep 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

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

- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [Neuro-Symbolic Data Generation for Math Reasoning](https://mlsanity.com/paper/2412.04857/) (2024)
- [Learning to Prove from Synthetic Theorems](https://mlsanity.com/paper/2006.11259/) (2020)
- [Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs](https://mlsanity.com/paper/2503.04772/) (2025)

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

- [Reasoning Core: A Scalable RL Environment for LLM Symbolic Reasoning](https://mlsanity.com/paper/2509.18083/) (2025)
- [Reasoning Core: A Scalable Procedural Data Generation Suite for Symbolic Pre-training and Post-Training](https://mlsanity.com/paper/2603.02208/) (2026)

## Abstract (arXiv)

The scarcity of high-quality, logically sound data is a critical bottleneck for advancing the mathematical reasoning of Large Language Models (LLMs). Our work confronts this challenge by turning decades of automated theorem proving research into a scalable data engine. Rather than relying on error-prone LLMs or complex proof-assistant syntax like Lean and Isabelle, our framework leverages E-prover's saturation capabilities on the vast TPTP axiom library to derive a massive, guaranteed-valid corpus of theorems. Our pipeline is principled and simple: saturate axioms, filter for "interesting" theorems, and generate tasks. With no LLMs in the loop, we eliminate factual errors by construction. This purely symbolic data is then transformed into three difficulty-controlled challenges: entailment verification, premise selection, and proof reconstruction. Our zero-shot experiments on frontier models reveal a clear weakness: performance collapses on tasks requiring deep, structural reasoning. Our framework provides both the diagnostic tool to measure this gap and a scalable source of symbolic training data to address it. We make the code and data publicly available. https://github.com/sileod/reasoning_core https://hf.co/datasets/reasoning-core/rc1