Humans can develop new theorems to explore broader and more complex
mathematical results. While current generative language models (LMs) have
achieved significant improvement in automatically proving theorems, their
ability to generate new or reusable theorems is still under-explored. Without
the new theorems, current LMs struggle to prove harder theorems that are
distant from the given hypotheses with the exponentially growing search space.
Therefore, this paper proposes an Automated Theorem Generation (ATG) benchmark
that evaluates whether an agent can automatically generate valuable (and
possibly brand new) theorems that are applicable for downstream theorem proving
as reusable knowledge. Specifically, we construct the ATG benchmark by
splitting the Metamath library into three sets: axioms, library, and problem
based on their proving depth. We conduct extensive experiments to investigate
whether current LMs can generate theorems in the library and benefit the
problem theorems proving. The results demonstrate that high-quality ATG data
facilitates models' performances on downstream ATP. However, there is still
room for current LMs to develop better ATG and generate more advanced and
human-like theorems. We hope the new ATG challenge can shed some light on
advanced complex theorem proving.

自动生成定理是一个挑战，本文提出了一个基于自动化定理生成（ATG）的评估基准，以探究当前生成性语言模型（LMs）在生成新定理和可重复定理方面的能力，结果表明当前 LMs 仍有改进空间。