ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev +1 more
2/24/2023
cs.CLcs.AIcs.LO

No official code found. Best implementation: EleutherAI/gpt-neox (7,470 stars, Apache-2.0, last commit 2026-04-13). 1 more below.

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.

View on arXivView PDF

Code Implementations(2)

EleutherAI/gpt-neoxCommunity100%
Apache-2.0

An implementation of model parallel autoregressive transformers on GPUs, based on the Megatron and DeepSpeed libraries

7,4701,127C, C++Dec 22, 20206 months agoApache-2.0
deepspeed-librarygpt-3language-modeltransformers
zhangir-azerbayev/ProofNetCommunity100%
MIT

Benchmark for undergraduate-level formal mathematics

12615TeX, LeanApr 4, 20222 years agoMIT

Similar Papers

IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch

88% match1 repo42025

A New Approach Towards Autoformalization

86% match1 repo62023

Reliable Evaluation and Benchmarks for Statement Autoformalization

86% match1 repo1322024

Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization

85% match2026

Theorem Prover as a Judge for Synthetic Data Generation

84% match2025

MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize

83% match2026

Cite this paper

@article{azerbayev2023proofnet,
  title  = {ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics},
  author = {Zhangir Azerbayev and Bartosz Piotrowski and Hailey Schoelkopf and Edward W. Ayers and Dragomir Radev and Jeremy Avigad},
  year   = {2023},
  eprint = {2302.12433},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2302.12433v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2302.12433.svg)](https://codeofpaper.com/paper/2302.12433)

Discussion