  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.
