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个定理，专门用于非关联形式化任务。我们欢迎社区为本数据集的后续版本提供任何贡献。