ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

Abstract

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.

Cited by in corpus (6)

• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers
• AutoMathKG: The automated mathematical knowledge graph based on LLM and vector database
• Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students
• Improving the Diproche CNL through Autoformalization via Large Language Models
• Proceedings 12th International Workshop on Theorem proving components for Educational software
• A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants