Verifying mathematical proofs is difficult, but can be automated with the
assistance of a computer. Autoformalization is the task of automatically
translating natural language mathematics into a formal language that can be
verified by a program. This is a challenging task, and especially for
higher-level mathematics found in research papers. Research paper mathematics
requires large amounts of background and context. In this paper, we propose an
avenue towards tackling autoformalization for research-level mathematics, by
breaking the task into easier and more approachable subtasks: unlinked
formalization (formalization with unlinked definitions and theorems), entity
linking (linking to the proper theorems and definitions), and finally adjusting
types so it passes the type checker. In addition, we present arXiv2Formal, a
benchmark dataset for unlinked formalization consisting of 50 theorems
formalized for the Lean theorem prover sampled from papers on arXiv.org. We
welcome any contributions from the community to future versions of this
dataset.

自动形式化研究级数学的一个方法是将任务分解为更容易和可接近的子任务：未链接的形式化、实体链接和类型调整。同时，本文还提出了一个用于未链接的形式化的基准数据集 arXiv2Formal，其中包含了从 arXiv.org 的论文中选取的 50 个定理的 Lean 定理证明器的形式化。欢迎社区为该数据集的未来版本做出贡献。