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论文中采样并为Lean定理证明器形式化的50个定理，专门用于无链接形式化研究。我们欢迎学术界对该数据集未来版本的任何贡献。