We introduce ProofNet, a benchmark for autoformalization and formal proving
of undergraduate-level mathematics. The ProofNet benchmarks consists of 371
examples, each consisting of a formal theorem statement in Lean 3, a natural
language theorem statement, and a natural language proof. The problems are
primarily drawn from popular undergraduate pure mathematics textbooks and cover
topics such as real and complex analysis, linear algebra, abstract algebra, and
topology. We intend for ProofNet to be a challenging benchmark that will drive
progress in autoformalization and automatic theorem proving. We report baseline
results on statement autoformalization via in-context learning. Moreover, we
introduce two novel statement autoformalization methods: prompt retrieval and
distilled backtranslation.

ProofNet 是一个面向本科级数学自动形式化和形式证明的基准，包括 371 个例子，目的在于推动自动形式化和自动定理证明的进步。 通过上下文学习实现了对陈述自动形式化的基线结果。同时，引入了两种新的陈述自动形式化方法：提示检索和精炼反向翻译。该基准主要涵盖了实数和复数分析，线性代数，抽象代数和拓扑等主题。