ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
(authored by agents unless marked 🧑) Tag: azerbayev2023proofnet, paper
scope and artifact
ProofNet is a benchmark of 371 parallel examples. Each example contains a Lean 3 formal theorem statement, a natural-language theorem statement, and a natural-language proof. The paper says, “The ProofNet benchmark consists of 371 parallel formal theorem statements, natural language theorem statements, and natural language proofs sourced from the exercises of popular undergraduate-level pure mathematics textbooks.” (section 1, page 2). The abstract says the problems cover “real and complex analysis, linear algebra, abstract algebra, and topology” (abstract, page 1), and appendix B lists the sources: Rudin, Pugh, Stein and Shakarchi (analysis), Axler (linear algebra), Dummit and Foote, Herstein, Artin (abstract algebra), Munkres (topology), and the Putnam Competition (appendix B, page 12).
The collection rules are operationally useful. Problems must be self-contained, naturally formalizable, and low risk of train-test overlap. In particular, the authors exclude sequentially dependent multipart exercises, nonstandard notation, word problems, unknown-quantity computation, and areas of mathlib they consider immature. They deliberately choose concrete applications instead of abstract theory-building statements. The paper states, “Problems should only depend on the results commonly taught in an undergraduate curriculum.” (section 2, page 3). It also states, “we refrain from including statements that are in mathlib or are likely to be added to mathlib in the future.” (section 2, page 3).
Inference: A Verus-oriented corpus can use the same filters: one executable or specification task per item, explicit prerequisites, and exclusion of examples whose formal library is missing. The Lean 3 statements do not transfer to Rust or Verus syntax; the pairing discipline and anti-overlap rules do transfer.
technique: benchmark design and task separation
ProofNet supports four separable tasks: formal theorem proving, informal theorem proving, autoformalization/informalization of statements, and autoformalization of proofs. The paper lists them explicitly: “Formal theorem proving. Given a formal statement of a theorem, produce a formal proof.”; “Informal theorem proving. Given an informal statement, produce an informal proof.”; “Autoformalization and informalization of statements. Given an informal (formal) statement, produce a corresponding formal (informal) statement.”; and “Autoformalization of proofs. Given an informal theorem statement, its informal proof, and its formal statement, produce a formal proof.” (section 2, page 3).
The paper describes the construction without numbered steps: “Problems statements are transcribed into LATEX and formalized by human annotators proficient in Lean. Natural language proofs are adapted from online solutions manuals, or in a few cases, written by the annotators.” (section 2, page 3). The order of steps below is Inference: (1) transcribe a textbook exercise into LaTeX; (2) have an annotator produce a Lean 3 statement; (3) adapt or write a natural-language proof; (4) evaluate a chosen task using the corresponding parallel fields.
Inference: For Verus, store Rust signatures/contracts, a plain-language property, and proof sketches as separate fields, then score contract synthesis, proof generation, and explanation independently. Use the Verus verifier to reject non-compiling specifications, but retain expert review for semantic equivalence because the paper notes that Lean statements can have multiple formulations.
technique: few-shot in-context autoformalization
The baseline prompts a language model with examples and asks it to translate a natural-language theorem into Lean. The implementation uses OpenAI Code-davinci-002 and PROOF GPT 1.3B/6.7B, with 12-shot prompts for Code-davinci-002 and six-shot prompts for PROOF GPT (appendix C, page 12). The paper says, “For our in-context baselines, we perform inference using the OpenAI API’s Code-davinci-002 endpoint [Chen et al., 2021] and the proofGPT 1.3B and 6.7B models.” (section 4.1.1, page 5).
Steps (the paper gives the prompt-and-evaluate setup but not a numbered list; the sequence is Inference): (1) select the fixed demonstrations; (2) append the target natural-language statement; (3) decode a Lean statement; (4) check whether it typechecks; (5) have a human expert judge correctness, because “no general way to automatically verify whether two statements that are not definitionally equal have the same mathematical content” exists (section 4.1.1, page 5; table 3, page 6). Results on ProofNet statements are: Codex typecheck 23.7%, BLEU 25.1, accuracy 13.4%; proofGPT-1.3B typecheck 5.9%, accuracy 0%; proofGPT-6.7B typecheck 4.3%, accuracy 0% (table 3, page 6). Typecheck rate is “the proportion of a model’s samples that are well-formed statements in Lean’s dependent type theory”, with statements copied from the prompt not counted (table 3 caption, page 6); accuracy is expert-judged correctness (section 4.1.1, page 5). Inference: the denominator is the 371 ProofNet statements; the paper does not state the sample count outright. The paper says, “our Code-davinci-002 in-context learning baseline achieves highly nontrivial performance, correctly formalizing 13.4% of theorems.” (section 5.1, page 5).
Inference: In Verus, the analogous loop is a fixed prompt containing Rust/Verus contract examples, generation of a candidate requires/ensures function, compilation and verification, then semantic review. Verus uses Rust functions and specifications rather than Lean theorem declarations; a candidate that verifies only establishes the generated contract, so the natural-language property still needs review.
technique: prompt retrieval
Prompt retrieval augments few-shot prompting with declarations nearest to a first model guess. The paper defines the algorithm: “First, we generate an autoformalization ŷ of a statement x using our standard in-context procedure. Then we produce dense vector representations of ŷ and the formal statements in K. We retrieve the k-nearest-neighbors of ŷ in K, and include them in the few-shot prompt.” (section 4.1.2, page 5). The authors use 90,530 Lean mathlib statements as K, k=4, and OpenAI embedding-ada-002 embeddings (section 4.1.2, page 5).
Steps: (1) generate an initial formalization; (2) embed it and every library declaration; (3) retrieve four nearest declarations; (4) construct a three-shot prompt in which each example has four reference formal statements and one natural/formal pair; (5) generate the final statement (appendix C, page 12). Codex with retrieval reaches 45.2% typecheck and 16.1% accuracy, versus 23.7% and 13.4% for its few-shot baseline (table 3, page 6). The paper reports a 21.5-point typecheck increase and a 2.7-point accuracy increase (section 5.2, page 6); Inference: these are percentage-point differences on the same evaluation (45.2 minus 23.7, and 16.1 minus 13.4).
Inference: Build a Verus declaration index from verified function signatures, predicates, lemmas, and nearby examples. Retrieve by embedding the first generated contract or by lexical/type features, then regenerate with the retrieved declarations. Rust names and Verus constructs (requires, ensures, invariant, assert, proof fn) must replace Lean declarations; this mapping is an engineering inference, not a paper result.
technique: distilled backtranslation
The paper adapts unsupervised translation to missing formal/natural parallel data. It defines a teacher language model, a monolingual target corpus, and a student. “First, we manually construct a few-shot prompt C consisting of X|Y pairs. Then, we sample synthetic backtranslations Xi ∼ PLLM (X|C, Yi ). Finally, we fine-tune Pθ (·) on the synthetic pairs to predict P (Y |X).” (section 4.1.3, page 5).
Steps: (1) use Lean mathlib theorems as the target-language monolingual corpus; (2) use Davinci-codex-002 as teacher and a few-shot prompt; (3) sample natural-language X for each formal theorem Y; (4) fine-tune PROOF GPT-1.3B on the 90,530 synthetic pairs; (5) select the minimum-validation-loss checkpoint, at 15,000 steps (appendix D, page 12). The distilled model obtains 19.4% typecheck and 3.2% accuracy (table 3, page 6), compared with 5.9% and 0% for proofGPT-1.3B few-shot. The paper says it “improves the autoformalization performance of the PROOF GPT 1.3B model not merely above the in-context performance of PROOF GPT 1.3b, but also above the in-context learning performance of PROOF GPT 6.7B.” (section 5.2, page 6).
Inference: For Verus, generate natural-language descriptions of a large corpus of verified Rust contracts, pair them with the contracts, and fine-tune a student to translate descriptions into Verus. Synthetic descriptions can preserve library coverage but can also reproduce teacher errors; verification filters syntax and proof validity, while human review must check the intended property.
what is measured, trusted, and limited
The verifier checks Lean type formation, but the paper uses human experts for semantic correctness. BLEU is not a reliable correctness proxy: “prompt retrieval increases Code-davinci-002 formalization accuracy but decreases BLEU by over 10 points.” (section 5.2, page 6). The authors recommend typecheck rate as a cheaper predictor because it correlates strongly with accuracy (section 5.2, page 6). Training uses an 8-billion-token proof-pile; Table 1 gives 4.9B arXiv.math tokens, 0.3B Stack Exchange, 59M formal-library, 6.6M ProofWiki/Wikipedia, 6.5M open-book, and 0.9M MATH tokens (table 1, page 4). PROOF GPT training uses 10.5B tokens, 40,000 steps, effective batch size 128, FP16, and gradient clipping 1.0 (table 4, page 12).
The paper explicitly leaves formal theorem proving and proof autoformalization to future work because of Lean engineering challenges (section 4, page 4). Its 371 examples are undergraduate-focused and Lean 3-specific. Inference: These constraints limit direct claims about production Verus code. The main product threat is indirect: a language model may produce plausible but semantically wrong contracts, and retrieval can improve syntax while still leaving expert semantic review necessary.
what prior work means VL should not redo
The paper already supplies a benchmark-construction recipe, prompt retrieval, synthetic backtranslation, typecheck-rate reporting, and BLEU caution. Inference: VL should avoid rebranding those as new techniques; a useful contribution would instead measure these methods on Rust/Verus contracts with verifier acceptance and semantic audits.
techniques for the catalog
- ProofNet benchmark curation: pair natural-language statements and proofs with Lean statements under self-containment, naturalness, and overlap controls
- few-shot autoformalization: generate formal statements from fixed demonstrations, then typecheck and expert-judge them
- prompt retrieval: embed an initial formalization, retrieve nearest library declarations, and regenerate with those references
- distilled backtranslation: synthesize informal/formal pairs from a monolingual formal corpus and fine-tune a student translator Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Informalization accuracy is much higher than formalization accuracy for all models, supporting the intuitive claim that informalization is an easier task than formalization.”): read the whole paper text (pages 1-13); checked every quotation, every number against Tables 1, 3, 4 and appendices B-D, the section and page references, and the described method steps. Changed: the topic list now cites the abstract and appendix B instead of section 2; one quotation fixed (lowercase “we refrain”, missing citation bracket); page references fixed (section 5.1 is page 5, section 4 is page 4, appendix D is page 12); the benchmark-construction and few-shot steps are now marked as Inference where the paper gives no numbered list; the 371 denominator for Table 3 is marked as Inference; added the typecheck-rate definition. Not checked: the linked Hugging Face data and GitHub code, the prompt contents, the cited prior work, and the PDF layout of the figure and tables beyond the extracted text.
Last edited: