“ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics”, Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad2023-02-24 (retrieval AI, knowledge distillation, Codex, dataset, math)⁠:

[model, data; Twitter] 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 analysis & 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 & distilled backtranslation.