# INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving

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

## Key facts

- Cited by 44 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Jul 2020.

## Built on by (most cited first, 30 of 44)

- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [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)
- [Exploring Length Generalization in Large Language Models](https://mlsanity.com/paper/2207.04901/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples](https://mlsanity.com/paper/2305.15269/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://mlsanity.com/paper/2101.06223/) (2021)
- [MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data](https://mlsanity.com/paper/2402.08957/) (2024)
- [Lyra: Orchestrating Dual Correction in Automated Theorem Proving](https://mlsanity.com/paper/2309.15806/) (2023)
- [TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models](https://mlsanity.com/paper/2310.10180/) (2023)
- [Mathematical Language Models: A Survey](https://mlsanity.com/paper/2312.07622/) (2023)
- [Subgoal Search For Complex Reasoning Tasks](https://mlsanity.com/paper/2108.11204/) (2021)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [Proving Olympiad Algebraic Inequalities without Human Demonstrations](https://mlsanity.com/paper/2406.14219/) (2024)
- [Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning](https://mlsanity.com/paper/2502.13834/) (2025)
- [A Symbolic Framework for Evaluating Mathematical Reasoning and Generalisation with Transformers](https://mlsanity.com/paper/2305.12563/) (2023)
- [Lila: A Unified Benchmark for Mathematical Reasoning](https://mlsanity.com/paper/2210.17517/) (2022)
- [Fast and Precise: Adjusting Planning Horizon with Adaptive Subgoal Search](https://mlsanity.com/paper/2206.00702/) (2022)
- [Mastering Symbolic Operations: Augmenting Language Models with Compiled Neural Networks](https://mlsanity.com/paper/2304.01665/) (2023)
- [A Survey on Mathematical Reasoning and Optimization with Large Language Models](https://mlsanity.com/paper/2503.17726/) (2025)
- [Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning](https://mlsanity.com/paper/2412.15184/) (2024)
- [Abstract Visual Reasoning: An Algebraic Approach for Solving Raven's Progressive Matrices](https://mlsanity.com/paper/2303.11730/) (2023)
- [REFACTOR: Learning to Extract Theorems from Proofs](https://mlsanity.com/paper/2402.17032/) (2024)

## Abstract (arXiv)

In learning-assisted theorem proving, one of the most critical challenges is to generalize to theorems unlike those seen at training time. In this paper, we introduce INT, an INequality Theorem proving benchmark, specifically designed to test agents' generalization ability. INT is based on a procedure for generating theorems and proofs; this procedure's knobs allow us to measure 6 different types of generalization, each reflecting a distinct challenge characteristic to automated theorem proving. In addition, unlike prior benchmarks for learning-assisted theorem proving, INT provides a lightweight and user-friendly theorem proving environment with fast simulations, conducive to performing learning-based and search-based research. We introduce learning-based baselines and evaluate them across 6 dimensions of generalization with the benchmark. We then evaluate the same agents augmented with Monte Carlo Tree Search (MCTS) at test time, and show that MCTS can help to prove new theorems.