ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
This work addresses the challenge of autoformalization and automatic theorem proving in mathematics, providing a benchmark to drive progress in this domain-specific area.
The authors introduced ProofNet, a benchmark of 371 examples for autoformalizing and formally proving undergraduate-level mathematics, and reported baseline results using in-context learning along with two novel autoformalization methods: prompt retrieval and distilled backtranslation.
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.