# IsarStep: a Benchmark for High-level Mathematical Reasoning

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Jun 2020.

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

- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://mlsanity.com/paper/2101.06223/) (2021)
- [A Symbolic Framework for Evaluating Mathematical Reasoning and Generalisation with Transformers](https://mlsanity.com/paper/2305.12563/) (2023)
- [SubgoalXL: Subgoal-based Expert Learning for Theorem Proving](https://mlsanity.com/paper/2408.11172/) (2024)
- [Diverse Inference and Verification for Advanced Reasoning](https://mlsanity.com/paper/2502.09955/) (2025)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)

## Abstract (arXiv)

A well-defined benchmark is essential for measuring and accelerating research progress of machine learning models. In this paper, we present a benchmark for high-level mathematical reasoning and study the reasoning capabilities of neural sequence-to-sequence models. We build a non-synthetic dataset from the largest repository of proofs written by human experts in a theorem prover. The dataset has a broad coverage of undergraduate and research-level mathematical and computer science theorems. In our defined task, a model is required to fill in a missing intermediate proposition given surrounding proofs. This task provides a starting point for the long-term goal of having machines generate human-readable proofs automatically. Our experiments and analysis reveal that while the task is challenging, neural models can capture non-trivial mathematical reasoning. We further design a hierarchical transformer that outperforms the transformer baseline.