ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

🎯 Pitch

Autoformalization models struggle to connect informal mathematics with formal Lean 3 code, but a simple prompt retrieval method nearly doubles their typecheck rate to 45%. By searching a math library for similar formal statements and injecting them into prompts, even modest gains in accuracy emerge—and only on problems the model already partially understands.

1. Executive Summary

This paper introduces ProofNet, a benchmark of 371 parallel natural language statements, natural language proofs, and Lean 3 formal theorem statements drawn from undergraduate mathematics textbooks, designed to evaluate autoformalization and formal theorem proving. Using the PROOFGPT models (1.3B and 6.7B parameters, fine-tuned on an 8-billion-token mathematical corpus) and OpenAI's Code-davinci-002, the authors establish in-context learning baselines and propose two novel autoformalization methods: prompt retrieval (retrieving semantically similar mathlib declarations to augment few-shot prompts) and distilled backtranslation (synthetically generating informal-formal pairs from a monolingual formal corpus to fine-tune a student model). Code-davinci-002 achieves 13.4% autoformalization accuracy in the few-shot setting, with prompt retrieval boosting accuracy to 16.1% and nearly doubling the typecheck rate from 23.7% to 45.2%, while distilled backtranslation lifts the 1.3B PROOFGPT model from 0% to 3.2% accuracy, establishing that both retrieval-augmented prompting and synthetic data generation improve autoformalization performance only on problems where the base model already demonstrates non-trivial semantic understanding of the formal mathematics involved.

2. Context and Motivation

The Core Problem: No Standardized Benchmark for Autoformalization

The fundamental gap this paper addresses is deceptively simple: there exists no standardized, parallel dataset for evaluating systems that translate between informal mathematics (natural language) and formal mathematics (theorem prover code). This gap is significant because autoformalization—the task of automatically converting natural language mathematical statements and proofs into the formal logic of an interactive theorem prover (ITP)—is a critical missing link between two largely disconnected research communities.

To understand why this matters, consider the two dominant paradigms for applying language models to mathematical reasoning:

The natural language paradigm. Researchers treat mathematical reasoning as a sequence-to-sequence problem in natural language: given an informal problem statement, generate an informal proof (Welleck et al., 2021, 2022; Lewkowycz et al., 2022). This approach has the massive advantage of data abundance—the internet contains vast corpora of natural language mathematics, including textbooks, Stack Exchange discussions, arXiv papers, and competition solutions. The Minerva model (Lewkowycz et al., 2022), for instance, was trained on hundreds of gigabytes of mathematical text and achieved strong performance on quantitative reasoning benchmarks. However, this paradigm suffers from a fundamental trust problem: there is no automatic way to verify the correctness of a natural language proof. You cannot execute natural language reasoning the way you can execute code. A model can generate a plausible-sounding but logically flawed argument, and no automated system will catch the error. Human evaluation is necessary, which is slow, expensive, and does not scale to the bootstrapping approaches (like expert iteration or reinforcement learning) that have driven progress in other AI domains.

The formal paradigm. Researchers embed language models within interactive theorem provers such as Lean, Metamath, Isabelle, or Coq (Yang and Deng, 2019; Polu and Sutskever, 2020; Polu et al., 2022; Jiang et al., 2022a). In this setting, the language model suggests proof steps (tactics or lemmas), and the ITP checks each step for logical correctness. This provides an automatic, perfect verifier: a proof is either formally correct or it isn't, with no ambiguity. This verification signal enables powerful bootstrapping techniques—GPT-f (Polu et al., 2022) uses expert iteration where the model generates many proof attempts, the ITP identifies which ones succeed, and the model is retrained on successful proofs, creating a positive feedback loop. The problem, however, is data starvation. Formal mathematical libraries like Lean's mathlib contain tens of thousands of theorems, but this pales in comparison to the natural language mathematics on the internet. Moreover, formal mathematics is labor-intensive to produce—it takes a human expert significantly longer to write a formal proof than an informal one—so the existing corpora grow slowly. Training a language model exclusively on formal mathematics data limits what it can learn about mathematical reasoning patterns.

Autoformalization: the missing bridge. Autoformalization promises to connect these two worlds. If we could reliably translate natural language mathematics into formal statements and proofs, we could leverage the abundance of internet-scale informal mathematics data to produce training signals that are grounded in formal verification. The vision, articulated by Szegedy (2020), is an autonomous system that reads informal mathematics from the web, formalizes it, verifies the formalization, and uses the verified formal proofs as training data for further improvement—creating a self-sustaining loop that doesn't require human formalization effort.

But here is the crux: autoformalization itself needs to be evaluated. Without a benchmark—a set of (informal statement, formal statement, informal proof) triples—researchers cannot measure progress, compare methods, or identify failure modes. This is the specific gap ProofNet fills.

Why This Gap Is Significant

The authors motivate the importance of autoformalization evaluation along several dimensions (Section 1, expanded through context):

The scaling argument for formal verification. As language models are deployed in increasingly consequential domains—scientific research, engineering design, medical reasoning, code generation—the cost of undetected errors grows. Mathematics is a domain where correctness matters absolutely; a single logical error invalidates an entire proof. The ITP verification guarantee eliminates a failure mode that is inherent to natural language reasoning systems. But to make formal verification practical, we need models that can operate in the formal setting, which requires autoformalization capabilities.

The knowledge representation challenge. The paper draws a critical distinction (Section 1, Figure 1) between two types of mathematical reasoning that existing benchmarks conflate. Competition and olympiad problems (miniF2F by Zheng et al., 2022; MATH by Hendrycks et al., 2021) test reasoning that depends on a small, fixed set of elementary concepts: integer arithmetic, basic algebra, counting, geometry. As the authors note, these problems "require complex reasoning" but depend on a "relatively small set of elementary facts." In contrast, modern research mathematics requires reasoning over a massive, growing body of theory comprising thousands of definitions, lemmas, and theorems. The authors cite the formalization of perfectoid spaces (Buzzard et al., 2020) in Lean 3, which depends on over 3,000 distinct theorems and definitions. This is a qualitatively different challenge: it's not just about logical deduction, but about retrieval and application of relevant background knowledge from an enormous library. An autoformalization system needs to know not just how to reason, but which existing formal definitions and lemmas to use, and how they are named and structured in the formal library.

The formal library navigation problem. As a concrete illustration, consider the case studies in Section 5.3. To formalize "every element not in an ideal M is a unit" (Case Study 1), the model must know that ideals are represented as the typeclass ideal R, that maximality is a predicate is_maximal not a separate type, that ideals coerce to sets for set-theoretic notation, and that "only maximal ideal" is naturally expressed as a universal quantification over all maximal ideals rather than a cardinality constraint. This is not just translation—it requires deep familiarity with the conventions, naming patterns, and representational choices of a specific formal library. mathlib alone contains tens of thousands of declarations, and choosing the right one is a non-trivial retrieval problem. Prior work on premise selection (Irving et al., 2016; Tworkowski et al., 2022; Wu et al., 2022b) addresses this for formal theorem proving, but autoformalization requires the same capability from the other direction: given an informal concept, find the formal declaration that represents it.

Where Prior Approaches Fall Short

The paper identifies specific limitations in existing work that ProofNet is designed to address:

No standard autoformalization benchmark. Prior to ProofNet, autoformalization was evaluated in ad-hoc ways. Wu et al. (2022a) demonstrated that large language models can autoformalize Isabelle theorem statements via in-context learning, but their evaluation was on a small, hand-selected set of examples without a standardized, reproducible test set. Jiang et al. (2022b) showed a method for autoformalizing proofs in Isabelle, but this relied on a performant automated theorem prover (Sledgehammer) that is not available for all ITPs (notably, Lean at the time of writing). Without a shared benchmark, it is impossible to compare different autoformalization approaches, track progress over time, or perform controlled ablation studies. Each paper evaluates on its own custom test cases, making the literature fragmented.

Existing formal theorem proving benchmarks test the wrong capability. Benchmarks like miniF2F (Zheng et al., 2022) evaluate formal theorem proving: given a formal statement, produce a formal proof. These are important, but they do not test autoformalization at all—the formal statement is provided, and the challenge is proof search. ProofNet is designed to evaluate the complementary task: given an informal statement (and optionally an informal proof), produce the formal statement. This tests a model's understanding of formal mathematical language, library knowledge, and cross-modal translation, not its ability to search for proofs.

Competition problems don't stress library-scale reasoning. As argued above, olympiad-level benchmarks like miniF2F and MATH focus on problems whose solutions draw from elementary mathematics. A model can perform well on these benchmarks while knowing only a small fraction of the formal library. ProofNet explicitly targets undergraduate-level textbook exercises that span real analysis, complex analysis, linear algebra, abstract algebra, and topology. These problems require models to reason with concepts from across the undergraduate curriculum—norms, inner products, Sylow subgroups, maximal ideals, topological spaces, continuous functions—and to correctly identify which formal declarations correspond to each concept. The authors frame this as an intermediate goal: "ProofNet falls short of requiring mastery of all of modern mathematics, but poses the still ambitious goal of reasoning over the core of an undergraduate mathematics" (Section 1). This is a stepping stone toward the harder problem of research-level autoformalization (like the perfectoid spaces example), but it's already significantly more demanding than competition-focused benchmarks.

Lack of parallel data inhibits supervised approaches. If large parallel corpora of (informal, formal) pairs existed, autoformalization could be approached as a standard supervised sequence-to-sequence problem with fine-tuning. But such corpora don't exist. The formal mathematics community is small, and formalizing a single advanced theorem can take weeks or months of expert effort. ProofNet itself consists of only 371 examples—far too few for fine-tuning a large language model from scratch. This data scarcity is the motivation for the paper's two proposed methods (prompt retrieval and distilled backtranslation), which both attempt to circumvent the need for large parallel corpora. Prompt retrieval does so by improving few-shot prompting through better example selection; distilled backtranslation does so by synthetically generating parallel training data from a monolingual formal corpus. Both methods are responses to the same constraint: we have abundant monolingual data in both natural language mathematics and formal mathematics, but negligible parallel data connecting them.

In-context learning works but is brittle. Wu et al. (2022a) showed that large language models can autoformalize with in-context learning, but performance is highly sensitive to the choice of few-shot examples. The authors of ProofNet explicitly acknowledge this limitation in Section 4.1.2: "few-shot learning performance is highly sensitive to the exact prompt that is used." A fixed, generic prompt with randomly chosen examples is unlikely to provide the model with the specific library knowledge needed to formalize a diverse set of problems spanning different mathematical domains. The prompt retrieval method is designed to address this brittleness by dynamically constructing prompts that include the mathlib declarations most relevant to the specific problem at hand.

How This Paper Positions Itself

ProofNet positions itself as infrastructure for the autoformalization research community, not as a single-method contribution. The paper makes this clear through its structure: the benchmark itself is the central contribution (Section 2), and the methods (prompt retrieval, distilled backtranslation) are presented as baselines that future work should improve upon. The paper explicitly leaves formal theorem proving and proof autoformalization on ProofNet to future work (Section 4), focusing its empirical evaluation on statement autoformalization—which is already challenging enough to reveal significant room for improvement (the best system achieves only 16.1% accuracy).

The paper also positions PROOFGPT (Section 3) as an open-source resource that is intentionally not state-of-the-art. The authors acknowledge this explicitly: "We regard the PROOFGPT model suite as inferior to the Minerva models" but hope the research community will benefit from open weights and a curated mathematical training corpus (the proof-pile). This is a deliberate tradeoff: PROOFGPT is not meant to compete with closed-source models like Minerva or Code-davinci-002, but to provide an accessible platform for researchers to experiment with autoformalization methods, particularly those that require fine-tuning (like distilled backtranslation).

Finally, the paper draws an explicit analogy to unsupervised machine translation (Section 4.1.3, Section 6). The data situation in autoformalization mirrors that of unsupervised machine translation before the development of methods like backtranslation (Lample et al., 2017): abundant monolingual data in each language (informal mathematics, formal mathematics), negligible parallel data. The distilled backtranslation method directly imports this analogy, using a strong few-shot model (Code-davinci-002) to generate synthetic informal-formal pairs that are then used to fine-tune a student model. The authors are candid that they view backtranslation as a "temporary hack" and anticipate that sufficiently powerful language models will eventually perform autoformalization purely via in-context learning—mirroring what happened in unsupervised machine translation, where few-shot prompting with very large models has proven "unreasonably effective" (Garcia et al., 2023). This positions ProofNet not as proposing a permanent solution, but as providing the evaluation infrastructure needed to determine when such scaling-driven solutions actually work.

3. Technical Approach

3.1 Reader Orientation

This paper constructs a benchmark (ProofNet) and a set of baseline methods for translating between informal mathematical language and formal Lean 3 code. The central engineering challenge is the near-complete absence of parallel informal-formal training data: the paper therefore explores methods that either make better use of the few available examples (prompt retrieval for in-context learning) or synthetically manufacture parallel data from abundant monolingual resources (distilled backtranslation). The "shape" of the solution is a two-pronged attack on data scarcity—improving what you can do with a few prompts, and generating synthetic training pairs where none exist—both evaluated against a shared benchmark of 371 human-annotated parallel examples.

3.2 Big-Picture Architecture (Diagram in Words)

The system has five major components connected in a pipeline from data to evaluation:

ProofNet Benchmark — 371 parallel triples of (natural language statement, natural language proof, Lean 3 formal statement) drawn from undergraduate textbook exercises, spanning analysis, algebra, linear algebra, and topology. Serves as the evaluation target for all autoformalization methods.
PROOFGPT Models — Decoder-only language models (1.3B, 6.7B parameters) fine-tuned on an 8-billion-token mathematical corpus (the proof-pile). Provide an open-source base model for experiments, particularly for methods requiring fine-tuning (distilled backtranslation).
Few-Shot Autoformalization Baseline — Uses in-context learning with fixed hand-constructed prompts containing 12 (Code-davinci-002) or 6 (PROOFGPT) example formal-informal pairs. Maps an informal statement to a formal statement via autoregressive generation.
Prompt Retrieval Module — Takes an initial coarse formalization, embeds it, retrieves the k-nearest-neighbor formal declarations from a database of 90,530 mathlib statements, and injects those retrieved declarations into a new few-shot prompt. This dynamically adapts the prompt content to the specific theorem being formalized.
Distilled Backtranslation Pipeline — Uses a strong few-shot teacher model (Code-davinci-002) to generate synthetic informal statements from a monolingual corpus of 90,530 formal mathlib theorems, then fine-tunes a smaller student model (PROOFGPT-1.3B) on the resulting synthetic pairs. This creates parallel training data from unpaired monolingual resources.

Information flows as follows: a natural language theorem enters the system → if using the baseline, it is formatted with fixed few-shot examples and fed to the language model → if using prompt retrieval, an initial formalization is generated, embedded via embedding-ada-002, matched against the mathlib embedding database, and retrieved declarations are injected into a new prompt → if using distilled backtranslation, the student model was pre-fine-tuned on synthetic pairs generated by the teacher, and generates the formalization directly → in all cases, the output Lean code is checked by a human expert for type correctness and semantic accuracy against the ground-truth formal statement in ProofNet.

3.3 Roadmap for the Deep Dive

First, the ProofNet benchmark construction: what defines a valid problem, why specific sourcing criteria matter, and how the data supports multiple evaluation tasks. This establishes what the methods are evaluated against.
Second, the PROOFGPT models and the proof-pile training corpus: what data they are trained on, why fine-tuning on mathematical text matters, and how they compare to base models and larger proprietary models. These are the "substrate" on which the autoformalization methods operate.
Third, the few-shot in-context learning baseline: prompt format, generation procedure, evaluation protocol, and the crucial distinction between typecheck rate and semantic accuracy. This is the simplest method and the benchmark against which improvements are measured.
Fourth, the prompt retrieval method: the two-stage generation and retrieval pipeline, the embedding model and mathlib knowledge base, the nearest-neighbor retrieval algorithm, and why retrieving against an initial formalization works better than retrieving against the natural language input.
Fifth, the distilled backtranslation method: the teacher-student setup, the synthetic data generation process, the fine-tuning procedure, and the unsupervised machine translation analogy that motivates it.
Sixth, the autoformalization-specific evaluation metrics (typecheck rate, BLEU, expert-judged accuracy) and why standard NLP metrics fail to capture the crucial semantic dimension of formal correctness.

3.4 Detailed, Sentence-Based Technical Breakdown

This is primarily a benchmark and empirical methods paper whose core technical contribution is the construction of a parallel informal-formal evaluation dataset and the development of two data-efficient methods that circumvent the lack of large parallel corpora: prompt retrieval for dynamic few-shot prompt construction and distilled backtranslation for synthetic parallel data generation.

The ProofNet Benchmark: Construction, Criteria, and Supported Tasks

The ProofNet benchmark is a dataset of 371 examples, each a triple consisting of a natural language theorem statement, a natural language proof, and a Lean 3 formal theorem statement. The problems are drawn primarily from exercises in popular undergraduate pure mathematics textbooks spanning four major areas: analysis (Rudin's Principles of Mathematical Analysis, Pugh's Real Mathematical Analysis, Stein and Shakarchi's Complex Analysis), linear algebra (Axler's Linear Algebra Done Right), abstract algebra (Dummit and Foote's Abstract Algebra, Herstein's Abstract Algebra, Artin's Algebra), and topology (Munkres' Topology). A small number of problems are sourced from the Putnam Competition.

Problem selection criteria. Not all textbook exercises are suitable for formalization. The authors apply three explicit inclusion filters (Section 2, "Dataset collection"):

Self-containment. "Problems should only depend on the results commonly taught in an undergraduate curriculum." This rules out multi-part problems where later parts depend on earlier parts (breaking their standalone evaluability) and problems using nonstandard notation that lacks a clear mathlib counterpart. Each problem must be evaluable in isolation without requiring context from other problems.
Naturality of formalization. Problems that are inherently difficult to express in dependent type theory are excluded. The paper specifically mentions "word problems" and "exercises that require computing an unknown quantity" as categories that do not lend themselves naturally to Lean formalization. Additionally, problems depending on relatively immature parts of mathlib—specifically Euclidean geometry and combinatorics—are excluded because the formal library support is insufficient for consistent formalization.
Low risk of train-test overlap. This is perhaps the most subtle criterion and one that distinguishes ProofNet from mathlib itself. Because language models are often pre-trained on internet corpora that include mathlib source code, including statements that already exist in mathlib (or are likely to be added) would confound evaluation: a model might reproduce a memorized formal statement rather than demonstrating genuine autoformalization ability. The solution is a stylistic shift: ProofNet avoids the "abstract theory-building style" of mathlib (general theorems about algebraic structures, topological properties, etc.) and instead selects problems that involve "applying general results to specific cases." Figure 1 illustrates this distinction with a concrete example:
- mathlib style (left panel): exists_subgroup_card_pow_prime, a general theorem about the existence of subgroups of prime-power order in finite groups, stated at maximum generality.
- ProofNet style (right panel): exercise_4_5_14, a specific problem asking to prove that a group of order 312 has a normal Sylow p-subgroup, which requires applying the general Sylow theorems to the particular number 312 and deducing the normal subgroup property.

This design choice means that ProofNet tests a model's ability to recognize which general theorems apply to a given concrete situation and to correctly instantiate them, rather than testing memory of existing formal statements.

Formalization and annotation. Problems 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. The formal statements are expressed in Lean 3 and depend on mathlib, meaning that correct formalizations must use the specific naming conventions, typeclass structures, and representational choices of the mathlib library.

Supported tasks. Because ProofNet includes formal statements, informal statements, and informal proofs, it supports evaluation of four distinct tasks (Section 2, "Supported Tasks"):

Formal theorem proving: Given a formal statement, produce a formal proof. This is the task that miniF2F (Zheng et al., 2022) evaluates; ProofNet provides a complementary test set focused on undergraduate-level theory rather than competition problems.
Informal theorem proving: Given an informal statement, produce an informal proof. This is the standard natural language mathematical reasoning task evaluated by benchmarks like MATH (Hendrycks et al., 2021).
Autoformalization and informalization of statements: Given an informal statement, produce a formal statement (autoformalization), or given a formal statement, produce an informal statement (informalization). This is the primary task evaluated in the current paper's experiments.
Autoformalization of proofs: Given an informal statement, its informal proof, and its formal statement, produce a formal proof. This is the capstone task that combines all three modalities; the paper leaves its evaluation to future work.

The paper's empirical investigation focuses exclusively on statement autoformalization and informalization, with the explicit note (Section 4) that formal theorem proving and proof autoformalization are deferred due to "the engineering challenges of implementing neural theorem proving systems in Lean."

The PROOFGPT Models and the Proof-Pile Training Corpus

The PROOFGPT models are decoder-only causal language models designed to serve as open-source baselines for mathematical text generation tasks, including autoformalization. Their construction involves two stages: a base model initialization and a mathematical fine-tuning phase.

Base initialization. The PROOFGPT models are initialized from Pythia weights (Biderman et al., 2023), specifically from a development version of the Pythia suite with slightly different hyperparameters than the publicly released versions. This accounts for the small parameter count discrepancy: PROOFGPT-1.3B versus Pythia-1.4B, and PROOFGPT-6.7B versus Pythia-6.9B. The authors note that "performance of the development versions of Pythia and the open-source versions are near-identical," so this discrepancy is not expected to materially affect results.

The proof-pile corpus. The fine-tuning corpus (detailed in Table 1) is an 8-billion-token dataset of mathematical text assembled from six sources:

Source	Size (GB)	Tokens
arXiv.math	13.6	4.9B
Stack Exchanges	0.96	0.3B
Formal math libraries	0.14	59M
ProofWiki + Wikipedia math	0.02	6.6M
Open source books	0.015	6.5M
MATH	0.002	0.9M

The dominant source by a large margin is arXiv.math (4.9 billion tokens, representing approximately 61% of the corpus), consisting of mathematical papers from the arXiv preprint server. Stack Exchange mathematics forums contribute 0.3 billion tokens. Formal math libraries (presumably including Lean's mathlib and other ITP libraries) contribute only 59 million tokens, reflecting the relative scarcity of formal mathematical text. The remaining 13 million tokens come from ProofWiki, Wikipedia mathematics articles, open-source mathematics textbooks, and the MATH dataset (Hendrycks et al., 2021).

The critical design choice here is the heavy skew toward informal mathematics. The proof-pile contains orders of magnitude more natural language mathematical text than formal text. This reflects the data landscape the paper is addressing: abundant informal mathematics, scarce formal mathematics. A model fine-tuned on this corpus will develop strong representations of mathematical concepts as they appear in natural language, but its exposure to formal Lean syntax and mathlib conventions is limited to the relatively tiny formal math libraries slice (59M tokens, or roughly 0.7% of the corpus). This explains why PROOFGPT models achieve zero formalization accuracy in few-shot settings (Table 3): they have strong semantic understanding of mathematics but insufficient exposure to Lean's syntax and mathlib's naming conventions to generate type-correct formal code.

Fine-tuning procedure. Training is performed using the GPT-NeoX library (Andonian et al., 2021) with hyperparameters specified in Table 4 (Appendix A). The key training configuration is:

Total tokens processed: 10.5 billion (1.3 epochs over the 8-billion-token corpus).
Training steps: 40,000.
Optimizer: Adam with betas (0.9, 0.95), epsilon 1×10⁻⁸, weight decay 0.1.
Learning rate: maximum 2×10⁻⁴ (1.3B) or 1.2×10⁻⁴ (6.7B), minimum 2×10⁻⁵ or 1.2×10⁻⁵, scheduled via cosine decay with 400 warm-up steps.
Effective batch size: 128.
Precision: FP16 with gradient clipping at 1.0.

Evaluation of PROOFGPT quality. Table 2 reports perplexity on held-out subsets of the proof-pile and its arXiv component, comparing PROOFGPT against equivalently-sized Pythia base models. On the arXiv.math test set, PROOFGPT-1.3B achieves 3.17 perplexity (vs. Pythia-1.4B's 3.82), and PROOFGPT-6.7B achieves 3.12 (vs. Pythia-6.9B's 3.36). These reductions in perplexity confirm that fine-tuning on domain-specific mathematical text improves the model's fit to the mathematical language distribution, which is a prerequisite for any downstream mathematical task including autoformalization.

However, the authors explicitly position PROOFGPT as "inferior to the Minerva models" (Section 3) on two grounds: Minerva was fine-tuned on an order of magnitude more mathematical text, and Minerva spans a larger parameter range. The value proposition of PROOFGPT is not state-of-the-art performance but open accessibility—open-source weights enable the research community to experiment with methods (like distilled backtranslation) that require model fine-tuning.

Few-Shot In-Context Learning Baseline

The simplest autoformalization method evaluated is direct few-shot prompting of a language model. This serves as the baseline against which the two novel methods (prompt retrieval, distilled backtranslation) are compared.

Prompt structure. A prompt consists of a sequence of example pairs, each pairing a natural language theorem statement with its Lean 3 formalization, followed by the target natural language statement to be formalized. The model generates the formal statement autoregressively, one token at a time, conditioning on the entire prompt prefix.

The specific prompts used are viewable in the open-source repository, but the paper reports the number of examples: 12-shot for Code-davinci-002 autoformalization and informalization, 6-shot for PROOFGPT models. The reduced shot count for PROOFGPT is a practical constraint: PROOFGPT has a context window of 2,048 tokens (compared to Code-davinci-002's 8,192 tokens), so only the last six examples from the 12-shot prompt are used when prompting PROOFGPT. This is an important confound: PROOFGPT's poor performance (0% accuracy) is partially attributable to having half as many examples, not just to its smaller parameter count. The paper does not disentangle these factors.

Generation and decoding. The paper does not specify decoding parameters (temperature, top-p, top-k, number of samples) for the few-shot generation. This is a notable omission because generation quality in code-like tasks is highly sensitive to decoding strategy. Based on the reported typecheck rates (23.7% for Code-davinci-002), we can infer that a substantial fraction of generated outputs are syntactically invalid Lean code, suggesting either greedy decoding or sampling with relatively high temperature.

For the distilled backtranslation student models, Appendix D specifies that evaluation is performed on "the minimum validation loss checkpoint, which occurs at 15,000 training steps." For few-shot models, no such checkpoint selection applies since there is no fine-tuning.

Evaluation protocol. Because there is "no general way to automatically verify whether two statements that are not definitionally equal have the same mathematical content" (Section 4.1.1), autoformalizations are evaluated for correctness by a human expert. The evaluator checks both that the generated statement is syntactically valid Lean (typechecks) and that it is semantically equivalent to the ground-truth formal statement in the ProofNet dataset. This human evaluation is necessary because:

Two Lean statements can be logically equivalent without being syntactically identical (different variable names, equivalent formulations of the same condition, different order of arguments).
A statement can typecheck (be valid Lean) but still be semantically incorrect (formalize a different theorem than intended).
Automatic equality checking in dependent type theory is limited to definitional equality, which is far too strict for evaluating autoformalization.

The human evaluation protocol imposes a scalability limitation: evaluating new autoformalization methods requires expert Lean knowledge and manual inspection of generated outputs, which is time-consuming and expensive. This is one motivation for the paper's recommendation (Section 5.2) that "typecheck rate be used as a predictor of autoformalization performance when evaluating accuracy is too costly."

Baseline results. Table 3 reports three metrics for the few-shot baseline:

Formalization accuracy: Code-davinci-002 achieves 13.4% (correct formalizations out of 371 test problems). PROOFGPT-1.3B and PROOFGPT-6.7B both achieve 0%.
Typecheck rate: The proportion of generated outputs that are well-formed Lean statements, excluding cases where the model simply copies a formal statement from the prompt. Code-davinci-002 achieves 23.7%, PROOFGPT-1.3B achieves 5.9%, PROOFGPT-6.7B achieves 4.3%.
BLEU score: BLEU-4 with smoothing, computed on whitespace-split tokens, comparing generated formalizations against ground-truth formalizations. Code-davinci-002 achieves 25.1, PROOFGPT models achieve 8.1 and 4.7 respectively.

A key observation from these numbers: roughly half of Code-davinci-002's type-correct generations are semantically correct (13.4% accuracy / 23.7% typecheck rate ≈ 0.57). The paper interprets this as evidence that "the model displays high accuracy conditional on having generated valid Lean" (Section 5.1), suggesting that the primary bottleneck for Code-davinci-002 is not semantic understanding of mathematics but rather generating syntactically valid Lean code that uses the correct mathlib identifiers with the correct typeclass constraints.

Informalization baseline. The paper also reports informalization results (formal → natural language), evaluated on the same three metrics (with "typecheck rate" replaced by "compile rate" for LaTeX compilation). Code-davinci-002 achieves 62.3% accuracy with a 100% compile rate, dramatically higher than formalization accuracy. This supports the intuitive claim that informalization is an easier task: generating fluent natural language is something language models are inherently good at, and the model does not need to navigate the strict syntactic constraints of Lean's dependent type theory.

Prompt Retrieval Method

The prompt retrieval method addresses a specific limitation of fixed few-shot prompts: a generic set of example formalizations cannot cover the diverse range of mathematical concepts, mathlib identifiers, and typeclass patterns needed to formalize problems across analysis, algebra, linear algebra, and topology. A problem about Sylow subgroups requires different formal vocabulary than a problem about orthogonal complements of subspaces. The core insight of prompt retrieval is to dynamically construct a prompt that includes the mathlib declarations most semantically relevant to the specific theorem being formalized.

The method operates in a two-stage pipeline (Section 4.1.2):

Stage 1: Coarse initial formalization. Given a natural language statement $x$ , the system first generates a preliminary formalization $\hat{y}$ using standard few-shot prompting with a generic, fixed prompt. This initial formalization is expected to be imperfect—it may use incorrect identifiers, miss typeclass constraints, or contain syntactic errors—but it captures the approximate semantic content of the theorem in Lean-like syntax. The authors do not specify which model or prompt is used for this initial generation, but the context implies it is the same Code-davinci-002 few-shot setup used for the baseline.

Stage 2: Retrieval against mathlib. The coarse formalization $\hat{y}$ is embedded into a dense vector space using OpenAI's text-embedding-ada-002 model. The target knowledge base $\mathcal{K}$ consists of 90,530 formal statements from Lean's mathlib, each similarly embedded. The system retrieves the $k$ -nearest-neighbors of $\hat{y}$ in this embedding space (with $k=4$ in all experiments). These retrieved formal statements—which are actual working Lean code from mathlib—are then included in a new few-shot prompt alongside the target natural language statement. The full generation is then performed with this augmented prompt.

Why retrieve against $\hat{y}$ rather than $x$ ? The paper reports that "this method was significantly more performant in our preliminary experiments" (Section 4.1.2). The likely explanation is that embedding models like text-embedding-ada-002 are trained primarily on natural language and general code, not specifically on (natural language, Lean) pairs. An informal mathematical statement and its formal counterpart may not be close in the embedding space because their surface forms are radically different—"prove that if x is nilpotent, then 1+x is a unit" looks nothing like theorem nilpotent_is_unit_add_one. However, an imperfect formalization like theorem nilpotent_add_one_is_unit is syntactically closer to actual mathlib code and will embed near the correct declarations. The coarse formalization $\hat{y}$ acts as a "pivot" that maps the natural language query into the formal embedding space, enabling effective nearest-neighbor retrieval. This is a clever exploitation of the embedding model's geometry: even if the embedding model doesn't understand the semantic equivalence between informal and formal formulations, it does place syntactically similar formal code near each other.

Prompt format. The retrieval-augmented prompt uses a 3-shot format, where each of the three examples consists of 4 reference formal statements (the retrieved neighbors) followed by one natural-language-to-formal pair. This means the prompt presents the model with patterns of related formal declarations and then asks it to produce a new formalization. The reduced shot count (3 vs. 12 for the baseline) may seem disadvantageous, but the retrieved examples are specifically tailored to the problem, making each example more informative than a random generic example.

Results. Table 3 shows that prompt retrieval increases Code-davinci-002's formalization accuracy from 13.4% to 16.1% (+2.7 percentage points, or roughly 20% relative improvement). More dramatically, the typecheck rate nearly doubles from 23.7% to 45.2% (+21.5 percentage points). This asymmetric improvement—typecheck rate increasing far more than accuracy—suggests that retrieval primarily helps the model generate syntactically valid Lean code by exposing it to correct mathlib usage patterns for the relevant mathematical domain. The BLEU score, counterintuitively, drops from 25.1 to 14.8, which the paper interprets as evidence that "just as with code, BLEU is a poor guide to formalization performance" (Section 5.2): retrieval helps the model produce semantically correct but lexically diverse formalizations that diverge from the ground-truth token sequence.

What retrieval cannot fix. Case Study 3 in Section 5.3 provides a concrete example of the method's limitations. For an exercise about orthogonal complements, both the baseline Code-davinci-002 and the retrieval-augmented version fail. The baseline correctly identifies that the theorem involves U.orthogonal and ⊤ (the top subspace) but misses the implicit hypothesis that the space must be an inner product space over ℝ or ℂ ([inner_product_space K V] and [is_R_or_C K]). Retrieval does not fix this because the retrieved mathlib statements about orthogonal complements presumably include the correct typeclass constraints, but the model fails to infer that these constraints must be added to the theorem's hypotheses. This reveals a fundamental limitation: retrieval can surface relevant declarations, but the model must still perform the logical reasoning to determine which typeclasses and hypotheses those declarations require, and this reasoning can fail even when the relevant information is in-context.

Distilled Backtranslation Method

Distilled backtranslation addresses the data scarcity problem from a fundamentally different angle. Rather than improving few-shot prompting, it synthetically generates parallel training data that can be used to fine-tune a model for autoformalization. The method is inspired by work in unsupervised machine translation, specifically the distilled backtranslation algorithm of Han et al. (2021a), and exploits the same asymmetry the paper identifies elsewhere: informal-to-formal is hard (the model must produce correct Lean syntax), but formal-to-informal is easier (producing natural language from formal code).

The unsupervised translation analogy. In unsupervised machine translation between two natural languages (say, English and French), parallel corpora are scarce but monolingual corpora in each language are abundant. The backtranslation approach (Lample et al., 2017) works as follows: train a source-to-target model on whatever parallel data exists, use it to translate monolingual target-language text back into the source language, then treat these synthetic backtranslations as additional training data for the target-to-source direction. The key insight is that the target language monolingual corpus provides authentic output-side examples—the model learns what good output looks like—even though the input-side synthetic backtranslations are imperfect.

Autoformalization has the same structure: formal mathematics (Lean code) is the "target language" with a moderate monolingual corpus (mathlib's 90,530 theorems); natural language mathematics is the "source language" with a vast monolingual corpus (arXiv, textbooks, etc.); and parallel data is negligible (ProofNet's 371 examples). The distilled backtranslation method adapts the unsupervised MT pipeline to this setting.

The three-step procedure (Section 4.1.3):

Step 1: Construct a few-shot teacher prompt. A manually constructed prompt $C$ consists of several $X|Y$ pairs, where each $X$ is a natural language theorem statement and each $Y$ is its formal Lean counterpart. The prompt is designed to elicit informalizations: when given a formal statement $Y_i$ , the model should generate a corresponding natural language statement $X_i$ .

Step 2: Generate synthetic backtranslations using the teacher. For each formal theorem $Y_i$ in the mathlib monolingual corpus (the target language), the teacher model samples a synthetic informal backtranslation:

$X_i \sim P_{\text{LLM}}(X \mid C, Y_i)$

where $P_{\text{LLM}}$ is the teacher language model (Code-davinci-002, accessed via the OpenAI API as the Code-davinci-002 endpoint). The symbol $\sim$ indicates sampling from the model's output distribution conditioned on the few-shot prompt $C$ and the formal statement $Y_i$ . For each of the 90,530 mathlib theorems, the teacher generates a natural language version, producing a synthetic parallel corpus of 90,530 $(X_i, Y_i)$ pairs. The teacher's output $X_i$ is an imperfect informalization—it may miss nuances, simplify assumptions, or produce slightly awkward mathematical English—but it captures the core mathematical content of the formal statement.

Step 3: Fine-tune the student model on synthetic pairs. A student model $P_\theta(Y \mid X)$ —in this case, PROOFGPT-1.3B—is fine-tuned to predict the formal statement $Y_i$ from the synthetic informal statement $X_i$ :

$\theta^* = \arg\max_\theta \sum_i \log P_\theta(Y_i \mid X_i)$

The training objective is standard autoregressive language modeling cross-entropy: the model is given the synthetic informal statement as input and trained to generate the corresponding formal statement token by token, with the loss computed only on the formal statement tokens.

Fine-tuning configuration (Appendix D, Table 5):

Training steps: 20,000
Learning rate: 5×10⁻⁵, scheduled via cosine decay with 2,000 warm-up steps.
Optimizer: AdamW with betas (0.9, 0.999), epsilon 1×10⁻⁸, weight decay 0.1.
Effective batch size: 24
Precision: FP16 with gradient clipping at 1.0.
Checkpoint selection: The "minimum validation loss checkpoint, which occurs at 15,000 training steps" is used for evaluation.

Why this should work. The backtranslation method leverages two properties of the problem structure:

Formal→informal is easier than informal→formal. Code-davinci-002 achieves 62.3% informalization accuracy (Table 3), dramatically higher than its 13.4% formalization accuracy. The teacher model can therefore generate reasonably high-quality synthetic informal statements from real formal statements, even if those informalizations are not perfect. The student model then learns from authentic formal outputs (real mathlib theorems) paired with noisy but semantically related informal inputs.
The formal output distribution is authentic. The student model is trained to produce real, human-written Lean code from mathlib, not synthetic formalizations. This means the student learns the correct target language distribution—proper mathlib conventions, typeclass usage patterns, naming schemes—even though its input-side training data is synthetic. This is the same principle that makes backtranslation effective in unsupervised MT: the target-side monolingual data provides authentic output examples, and the synthetic source-side data provides enough signal to learn the cross-modal mapping.

A crucial detail: the teacher and student use different interface access patterns. The teacher (Code-davinci-002) is used only for inference via the OpenAI API to generate synthetic data. The student (PROOFGPT-1.3B) is fine-tuned on weights that are open-source and accessible for training. This makes the method reproducible: once the synthetic data is generated (a one-time cost), the student fine-tuning can be performed entirely with open models. This is a practical advantage over relying on proprietary APIs for deployment.

Results. Table 3 shows that distilled backtranslation lifts PROOFGPT-1.3B from 0% formalization accuracy (few-shot baseline) to 3.2% accuracy. The typecheck rate increases from 5.9% to 19.4%, and BLEU score increases from 8.1 to 10.7. While 3.2% accuracy is far below Code-davinci-002's 13.4% or 16.1% (with retrieval), the result is significant because it demonstrates that a relatively small model (1.3B parameters) can acquire non-trivial autoformalization capability through purely synthetic training data—without ever seeing a real human-written informal-formal pair during fine-tuning. This validates the core premise of the distilled backtranslation approach: synthetic parallel data can provide a weak but real training signal for autoformalization.

Limitations of the approach. The 3.2% accuracy is low in absolute terms, and the method depends on access to a strong teacher model (Code-davinci-002) that already has some autoformalization capability. This creates a circular dependency: you need a model that can autoformalize (at least in the easier formal→informal direction) to train a model that can autoformalize. The method amplifies the teacher's capability rather than creating it from scratch. Furthermore, the synthetic informalizations contain errors that propagate into the student's training data, creating a ceiling on achievable performance that depends on the teacher's quality.

The authors themselves express ambivalence about backtranslation as a long-term solution: "the authors of this work regard backtranslation as a temporary hack and foresee that in-context learning will be enough to elicit maximal performance from a sufficiently good language model" (Section 6). This prediction is based on the trajectory observed in unsupervised machine translation, where scaling up few-shot prompting with very large models has proven "unreasonably effective" (Garcia et al., 2023). The implication is that ProofNet's value as a benchmark will persist even if backtranslation becomes obsolete, because it provides the evaluation infrastructure needed to compare few-shot autoformalization capabilities across models and prompt engineering strategies.

Evaluation Metrics for Autoformalization

The paper reports three distinct metrics for autoformalization performance, each capturing a different dimension of model capability. Understanding the relationships among these metrics is essential to interpreting the experimental results.

Typecheck rate (and compile rate). Typecheck rate is the proportion of a model's generated outputs that are syntactically valid Lean statements—that is, they parse and typecheck successfully in Lean 3's dependent type theory. To prevent gaming the metric, outputs that simply copy a formal statement from the few-shot prompt are excluded from the numerator. The paper reports typecheck rates ranging from 4.3% (PROOFGPT-6.7B) to 45.2% (Code-davinci-002 with prompt retrieval).

What typecheck rate measures: A model's ability to generate code that respects Lean's grammar, type system rules, and mathlib's API conventions. This includes using identifiers that actually exist in mathlib, applying typeclass constraints correctly, getting the order of arguments right, and respecting implicit/explicit argument conventions. Generating type-correct Lean is a non-trivial feat because Lean's dependent type theory is expressive and strict—incorrect code is caught at compile time, not at runtime.

What typecheck rate does NOT measure: Semantic correctness. A statement can be perfectly valid Lean while formalizing a completely different theorem than intended. Case Study 3 illustrates this: theorem exercise_6_16 ... : U.orthogonal = {0} ↔ U = ⊤ typechecks but is semantically wrong because it fails to require an inner product space structure.

BLEU score. BLEU-4 (Papineni et al., 2002) with smoothing is computed on whitespace-split tokens, comparing the generated formalization to the ground-truth formalization in ProofNet. The paper reports BLEU scores ranging from 4.7 (PROOFGPT-6.7B) to 25.1 (Code-davinci-002 baseline).

What BLEU measures: Token-level n-gram overlap between the generated and reference formalizations. This captures surface-level lexical similarity.

What BLEU does NOT measure reliably: Semantic equivalence. The paper explicitly states that "BLEU is a poor guide to formalization performance" (Section 5.2), as demonstrated by the prompt retrieval result: retrieval increases accuracy from 13.4% to 16.1% but decreases BLEU from 25.1 to 14.8. The explanation is that retrieval helps the model produce semantically correct formalizations that use different identifier names, argument orders, or syntactic formulations than the ground truth, reducing n-gram overlap while improving correctness.

The paper also notes that BLEU scores are systematically higher for formalization than informalization (e.g., 25.1 vs. 13.2 for Code-davinci-002), but this is "likely because natural language contains more lexically distinct but semantically equivalent statements." Formal Lean code has more constrained vocabulary—there are only so many ways to say is_maximal M in Lean—while natural language has many paraphrases for the same mathematical claim.

Expert-judged accuracy. The gold-standard metric, and the only one that directly measures what we care about: what fraction of generated formalizations are semantically equivalent to the ground-truth formal statement in ProofNet? A human expert with Lean proficiency evaluates each generated output. The paper reports accuracies from 0% (PROOFGPT few-shot) to 16.1% (Code-davinci-002 with prompt retrieval).

Correlations among metrics. The paper's analysis of these correlations (Section 5.2) yields two actionable insights:

Typecheck rate correlates strongly with accuracy. As noted above, roughly half of Code-davinci-002's type-correct generations are semantically correct. This makes typecheck rate a practical proxy metric: when human evaluation is too costly or slow, typecheck rate can serve as a rough indicator of autoformalization performance. The recommendation is explicitly made: "we recommend that typecheck rate be used as a predictor of autoformalization performance when evaluating accuracy is too costly."
BLEU does not reliably correlate with accuracy. The prompt retrieval result shows BLEU moving in the opposite direction from accuracy. This mirrors findings in code generation (Chen et al., 2021), where BLEU similarly fails to capture functional correctness. The paper's interpretation is that autoformalization is more like code generation than like natural language translation in this respect: small lexical differences can have large semantic consequences (using simple_group vs. is_simple_group changes correctness completely but barely affects BLEU), while large lexical differences can preserve semantic content (reordering arguments, using different but equivalent formulations).

Why these metrics matter for benchmark design. ProofNet is designed to be a shared benchmark for the autoformalization community. The metrics discussion reveals a tension: the only truly reliable metric (expert-judged accuracy) is expensive and slow, making rapid iteration difficult, while the cheap automatic metrics (typecheck rate, BLEU) are imperfect proxies that can mislead. Part of the paper's contribution is characterizing how these proxies mislead, so that future researchers can interpret them appropriately. The key practical takeaway is: track all three, treat typecheck rate as your primary automatic progress indicator, never trust BLEU alone, and periodically validate with expert judgment.

4. Key Insights and Innovations

Innovation 1: The Benchmark Itself as an Intellectual Contribution — Reframing Autoformalization as a Library-Knowledge Problem, Not a Reasoning Problem

Prior to ProofNet, autoformalization evaluation was fragmented and ad-hoc. Wu et al. (2022a) demonstrated in-context autoformalization in Isabelle but evaluated on a hand-selected, non-standardized set of examples. Each paper tested on its own custom problems, making cross-method comparison impossible and obscuring whether progress was genuine or an artifact of test-set idiosyncrasy. But ProofNet's deeper conceptual contribution is not simply providing a standardized test set — it is redefining what autoformalization difficulty means.

The dominant existing formal theorem proving benchmarks — miniF2F (Zheng et al., 2022) for formal proving, MATH (Hendrycks et al., 2021) for informal reasoning — frame mathematical difficulty in terms of reasoning depth: how many logical steps, how much creativity, how subtle the argument. These benchmarks use olympiad and competition problems where the core challenge is finding a clever proof strategy from elementary axioms. ProofNet makes a diagnostic move that the paper's framing (Section 1, Figure 1) crystallizes: at the undergraduate level and above, mathematical difficulty is increasingly defined by knowledge breadth, not just reasoning depth. You don't just need to think clearly — you need to know what a Sylow subgroup is, how it's represented in mathlib, whether maximality is a type or a predicate, and that orthogonal complements require an inner product space structure over ℝ or ℂ. This is a fundamentally different capability, and one that prior benchmarks were not designed to test.

The Figure 1 comparison between a typical mathlib theorem and a ProofNet problem makes this distinction concrete. The mathlib theorem (exists_subgroup_card_pow_prime) states a general result at maximum abstraction. The ProofNet problem (exercise_4_5_14) asks: "Prove that a group of order 312 has a normal Sylow p-subgroup." The intellectual challenge is not deep logical deduction per se — it's recognizing that the Sylow theorems apply to |G| = 312, instantiating the general theory to the specific number, and correctly navigating mathlib's representation of Sylow subgroups, normality, and finiteness constraints. This requires what the paper calls "reasoning over the core of an undergraduate mathematics" — a knowledge base comprising hundreds of definitions, theorems, and representational conventions, not just a handful of elementary axioms.

This reframing has a specific evidentiary anchor in the experimental results: Code-davinci-002's failure modes (Section 5.3, Case Studies 1-4) are predominantly library-knowledge failures, not reasoning failures. The model correctly infers that "only maximal ideal" should be a universal quantification (reasoning success) but uses the nonexistent identifier simple_group instead of is_simple_group (library-knowledge failure). It correctly formalizes orthogonal complement notation but misses that an inner product space typeclass constraint is required (implicit hypothesis failure). These are retrieval and convention problems, not deduction problems. The prompt retrieval method's asymmetric improvement — typecheck rate nearly doubles (+21.5 points) while accuracy gains are modest (+2.7 points) — is direct evidence that addressing the library-knowledge bottleneck (by retrieving relevant mathlib declarations) disproportionately helps with syntactic and conventional correctness, while semantic reasoning remains the harder ceiling.

This innovation is fundamental, not incremental: it changes what researchers should optimize for. If difficulty is primarily about library knowledge, then progress requires better premise retrieval, larger-context models that can ingest relevant library documentation, and training objectives that incentivize correct identifier usage — not just better reasoning architectures.

The prompt retrieval method contains a non-obvious technical insight that the paper understates but which has broader implications beyond autoformalization: when the embedding space doesn't align between source and target modalities, use an imperfect intermediate generation in the target modality as a pivot for retrieval. This is a genuinely clever solution to a specific cross-modal retrieval problem.

The standard approach for retrieval-augmented generation would embed the query (the natural language theorem) and retrieve against the knowledge base (the formal mathlib statements). The paper reports that this performed poorly in preliminary experiments. The likely reason is a modality gap: text-embedding-ada-002 is trained primarily on natural language and general code, so a natural language theorem ("every element not in M is a unit") and its formal counterpart (∀ x : R, x ∉ M → is_unit x) may not be close in embedding space despite being semantically equivalent — their surface forms are radically different.

The pivot strategy (Section 4.1.2) sidesteps this by generating a coarse formalization \hat{y} first — even an imperfect one that doesn't typecheck — and embedding that against the mathlib database. The coarse formalization, being syntactically closer to real Lean code, will embed near correct mathlib declarations. The method thus exploits the embedding model's sensitivity to syntactic surface form in a productive way: rather than fighting the modality gap, it translates the query into the target modality first (even imperfectly) and then retrieves in a space where proximity correlates with genuine relevance.

This has implications beyond autoformalization. Any cross-modal retrieval task where (a) generation in the target modality is easier than perfect translation, and (b) the embedding model is more sensitive to surface form than deep semantics, could benefit from this pivot strategy. Examples include: retrieving code snippets from natural language descriptions (generate rough pseudocode first, then retrieve real code against it), retrieving formal specifications from informal requirements, or retrieving mathematical formulas from natural language queries. The paper doesn't develop this into a general principle, but the pattern is recognizable and transferable.

The evidence for this innovation's effectiveness is the prompt retrieval results (Table 3): the method increases typecheck rate from 23.7% to 45.2% — nearly doubling — while also improving accuracy. The Case Study 2 (Section 5.3) provides a granular illustration: vanilla Code-davinci-002 uses the nonexistent simple_group identifier, but the retrieval-augmented version correctly uses is_simple_group because one of the 4 retrieved mathlib statements explicitly contains that declaration. This is a direct demonstration of the pivot strategy fixing a specific library-knowledge error.

This innovation is incremental in mechanism (retrieval augmentation is well-established) but fundamental in its diagnostic content: it identifies why cross-modal retrieval fails for autoformalization specifically and demonstrates a remedy that exploits the task structure rather than requiring a better embedding model.

Innovation 3: Distilled Backtranslation as a Viable Training Strategy in the Near-Complete Absence of Parallel Data

The distilled backtranslation method (Section 4.1.3) adapts unsupervised machine translation techniques to autoformalization, but its significance goes beyond the specific adaptation. What makes this result intellectually distinctive is that it demonstrates a 1.3B-parameter model can acquire non-trivial autoformalization capability (3.2% accuracy) from purely synthetic training data, without ever seeing a single real human-written informal-formal pair during fine-tuning. Every training example is a synthetic informalization generated by Code-davinci-002 from a real mathlib formal theorem.

Prior to this result, the default assumption in the autoformalization literature was that parallel data scarcity was a hard blocker for supervised approaches. Wu et al. (2022a) relied entirely on in-context learning with proprietary models precisely because fine-tuning was assumed infeasible without parallel corpora. Jiang et al. (2022b) required an external automated theorem prover as a verification oracle, adding infrastructure complexity. The distilled backtranslation result — while modest in absolute performance (3.2% vs. 13.4% for few-shot Code-davinci-002) — demonstrates that the assumed impossibility of supervised autoformalization training was too pessimistic. Synthetic data can provide a training signal, and that signal improves with better teacher models.

This connects to the paper's broader intellectual framing (Section 6): the authors explicitly analogize autoformalization to unsupervised machine translation circa 2017-2021, where backtranslation was the dominant paradigm before few-shot prompting with very large models became "unreasonably effective" (Garcia et al., 2023). The prediction — that backtranslation is a "temporary hack" that will be superseded by in-context learning at scale — positions this result as a waypoint, not a destination. But the waypoint is meaningful: it shows that the data bottleneck can be loosened without requiring human annotation, and it provides a reproducible recipe (teacher API access + open-source student fine-tuning) that researchers can immediately use and improve.

The evidence is in Table 3: PROOFGPT-1.3B goes from 0% accuracy (few-shot) to 3.2% (distilled backtranslation), with typecheck rate rising from 5.9% to 19.4%. The fact that a 1.3B model can achieve any non-zero accuracy through purely synthetic training is the surprising result — prior expectations would have predicted near-zero regardless of training methodology for a model of this scale on this task.

This innovation is incremental in method (backtranslation is well-established in MT) but fundamental in its empirical finding: it establishes a lower bound on what synthetic-data-only approaches can achieve and creates a clear target for improvement through better teacher models and larger student models.

Innovation 4: The Typecheck Rate as a Cheap, Reliable Proxy Metric for Autoformalization Progress

The paper's analysis of evaluation metrics (Section 5.2) might seem like a minor methodological contribution, but it solves a genuine practical bottleneck for autoformalization research. The gold-standard metric — expert human evaluation of semantic correctness — is slow, expensive, and requires Lean expertise that most ML researchers lack. If every ablation, hyperparameter sweep, and model comparison requires a human expert to judge hundreds of formalizations, research velocity grinds to a halt. Automatic surface-form metrics like BLEU are attractive because they're cheap and fast, but the paper demonstrates conclusively that BLEU is anti-correlated with accuracy in important regimes.

The diagnostic evidence is the prompt retrieval result (Table 3): retrieval increases accuracy from 13.4% to 16.1% (+20% relative) but decreases BLEU from 25.1 to 14.8 (-41% relative). A researcher optimizing BLEU would reject prompt retrieval as harmful; a researcher measuring accuracy would adopt it. This is not a weak correlation — it's a directionally wrong signal. The paper explains why: retrieval helps the model use correct mathlib identifiers and typeclass patterns that differ from the ground-truth formulation, reducing n-gram overlap while improving correctness. This mirrors findings in code generation (Chen et al., 2021), but the paper provides the first systematic evidence for the formal mathematics domain specifically.

The constructive contribution is the recommendation to use typecheck rate as the primary automatic proxy. The empirical justification: roughly half of Code-davinci-002's type-correct generations are semantically correct (13.4% / 23.7% ≈ 0.57), and typecheck rate correlates directionally with accuracy across methods (prompt retrieval increases both, distilled backtranslation increases both relative to the PROOFGPT few-shot baseline). Typecheck rate has the practical advantage of being fully automatic — it requires only running Lean's typechecker, which is fast and objective — and captures a meaningful intermediate capability (generating syntactically valid Lean with correct mathlib identifier usage).

This innovation is incremental in scope (it's a methodological recommendation, not a new algorithm) but practically fundamental for the autoformalization research community that ProofNet aims to serve. Without a cheap, reliable progress indicator, benchmark-driven research stagnates between expensive evaluation rounds. The typecheck rate recommendation — with the caveat that it's a proxy, not a substitute, and should be periodically validated against human judgment — provides exactly such an indicator.

The evidence is correlational rather than causal (the paper doesn't systematically vary typecheck rate independently), but the consistency of the relationship across three very different methods (few-shot, retrieval, backtranslation) and two model families (Code-davinci-002, PROOFGPT) strengthens the claim beyond coincidence.

5. Experimental Analysis

Evaluation Methodology

Dataset. ProofNet consists of 371 parallel examples, each containing a natural language theorem statement, a natural language proof, and a Lean 3 formal theorem statement, drawn from undergraduate-level pure mathematics textbook exercises across analysis (Rudin, Pugh, Stein and Shakarchi), linear algebra (Axler), abstract algebra (Dummit and Foote, Herstein, Artin), and topology (Munkres), with a small number from the Putnam Competition (Section 2, Appendix B). The full 371 examples are used as the test set; there is no described train/validation/test split since the primary evaluation methods are in-context learning and fine-tuning on external synthetic data, not fine-tuning on ProofNet itself.
Base model(s). Three language model families are evaluated: (1) Code-davinci-002, accessed via the OpenAI API, representing a large proprietary code-and-language model with an 8,192-token context window; (2) PROOFGPT-1.3B and PROOFGPT-6.7B, decoder-only causal language models initialized from Pythia development weights and fine-tuned on the proof-pile, an 8-billion-token corpus of mathematical text, with 2,048-token context windows (Section 3, Table 1, Table 2). The PROOFGPT models are explicitly positioned as open-source baselines that the authors "regard as inferior to the Minerva models" due to training on an order of magnitude less mathematical text (Section 3), chosen to provide an accessible platform for methods requiring fine-tuning (like distilled backtranslation) rather than to compete with proprietary models.
Metrics. Three metrics are reported for autoformalization (Table 3): (1) Expert-judged accuracy — the fraction of generated formal statements that a human expert proficient in Lean judges to be semantically equivalent to the ground-truth formal statement in ProofNet, necessary because "there is no general way to automatically verify whether two statements that are not definitionally equal have the same mathematical content" (Section 4.1.1); (2) Typecheck rate — the proportion of generated outputs that are well-formed Lean statements passing Lean 3's typechecker, excluding cases where the model simply copies a formal statement from its prompt; (3) BLEU-4 score — computed with smoothing on whitespace-split tokens, comparing generated formalizations to ground-truth formalizations. For informalization, accuracy is expert-judged and "compile rate" (proportion of outputs that produce compilable LaTeX) substitutes for typecheck rate.
Baselines. The primary baseline is few-shot in-context learning (Section 4.1.1), using manually constructed prompts: 12-shot for Code-davinci-002, 6-shot for PROOFGPT models (reduced due to the 2,048-token context window). This baseline is not attributed to prior work as a specific method, though it follows the in-context learning paradigm of Brown et al. (2020). The paper also implicitly treats the vanilla PROOFGPT few-shot results (0% accuracy) as a baseline for distilled backtranslation, which fine-tunes the same PROOFGPT-1.3B model.
Generation budget / compute accounting. Generation budget is not explicitly quantified in terms of FLOPs or inference cost. The fair comparison axis is implicit: all methods are evaluated on the same 371-example test set, and differences in method complexity (few-shot API calls, retrieval with embedding and re-prompting, fine-tuning on synthetic data) are not converted to a common cost metric. The paper does not report decoding parameters (temperature, sampling strategy, number of samples per prompt), making precise reproduction of generation costs impossible from the text alone. For distilled backtranslation, the training budget is reported in terms of fine-tuning steps (20,000 steps with effective batch size 24, Appendix D, Table 5) and the one-time cost of generating 90,530 synthetic backtranslations from Code-davinci-002.
Cross-validation / statistical protocol. There is no cross-validation, statistical significance testing, or confidence interval reporting for the autoformalization accuracy results. The evaluation is a single pass over the 371-example test set with human expert judgment for each generated output. The absence of statistical rigor is a practical consequence of the expense of human evaluation—running multiple trials with different random seeds or prompt permutations and having an expert judge each would multiply an already costly evaluation—but it means that differences of a few percentage points (e.g., 13.4% vs. 16.1%) should be interpreted cautiously as they may not be statistically significant. For distilled backtranslation, model selection uses the "minimum validation loss checkpoint, which occurs at 15,000 training steps" (Appendix D), but no details are provided about the validation set composition or size.

Main Quantitative Results

The experimental evaluation is organized around two axes: (1) the few-shot in-context learning baseline for both autoformalization and informalization, establishing the performance floor and ceiling across model scales, and (2) the two proposed methods—prompt retrieval and distilled backtranslation—each evaluated against the few-shot baseline on autoformalization only.

Few-Shot Autoformalization and Informalization

The headline result (Table 3, "Few-shot" rows) is that Code-davinci-002 achieves 13.4% autoformalization accuracy on ProofNet statements, while PROOFGPT models at both scales achieve 0%. The 13.4% figure represents 50 out of 371 statements correctly formalized—non-trivial but far from reliable performance. The 0% for PROOFGPT models means that not a single generated formalization was judged semantically correct by the human evaluator.

The typecheck rate breakdown reveals a more nuanced picture. Code-davinci-002 achieves 23.7% typecheck rate, meaning that approximately one in four generated outputs is syntactically valid Lean code. The ratio of accuracy to typecheck rate (13.4 / 23.7 ≈ 0.57) indicates that roughly half of the model's type-correct outputs are semantically correct—the other half are valid Lean that formalizes the wrong theorem. PROOFGPT 1.3B achieves 5.9% typecheck rate and PROOFGPT 6.7B achieves 4.3%, showing that even the larger PROOFGPT model struggles to generate syntactically valid Lean, and the slight degradation from 1.3B to 6.7B (5.9% to 4.3%) is unexpected and unexplained.

BLEU scores follow the same ranking: Code-davinci-002 at 25.1, PROOFGPT-1.3B at 8.1, PROOFGPT-6.7B at 4.7. The substantial gap between Code-davinci-002 (25.1) and the PROOFGPT models (8.1, 4.7) mirrors the accuracy gap, but the paper explicitly warns against interpreting BLEU as a reliable quality indicator (Section 5.2).

For informalization (formal → natural language), the performance landscape inverts. Code-davinci-002 achieves 62.3% accuracy with a 100% compile rate (every generated informalization produces compilable LaTeX). PROOFGPT-1.3B achieves 4.3% accuracy and PROOFGPT-6.7B achieves 6.5% accuracy, with compile rates of 0.77% and 0.70% respectively. The compile rate is low for PROOFGPT models primarily because their generations contain Unicode characters frequently used in Lean's mathlib (e.g., Greek letters, mathematical symbols) that are not accepted by the pdflatex compiler. The BLEU scores are lower for informalization than formalization (13.2 for Code-davinci-002 vs. 25.1 for formalization), which the paper attributes to natural language containing "more lexically distinct but semantically equivalent statements" (Table 3 notes).

The large gap between informalization accuracy (62.3%) and formalization accuracy (13.4%) for Code-davinci-002 supports the paper's framing that formalization is the harder direction—the model has strong semantic understanding of formal mathematics (it can explain what a formal theorem says in natural language) but struggles to produce correct formal syntax.

Prompt Retrieval Results

Prompt retrieval is evaluated only on Code-davinci-002 for autoformalization (Table 3, "Prompt retrieval" row). The method increases accuracy from 13.4% (baseline) to 16.1% (+2.7 percentage points), representing a roughly 20% relative improvement. More dramatically, the typecheck rate nearly doubles from 23.7% to 45.2% (+21.5 percentage points). This is the most striking single result in the table: retrieval-augmented prompting makes the model roughly twice as likely to produce syntactically valid Lean code.

The BLEU score, however, decreases from 25.1 to 14.8 (a drop of 10.3 points). The paper interprets this as evidence that "just as with code, BLEU is a poor guide to formalization performance"—retrieval helps the model produce correct formalizations that are lexically different from the ground truth, reducing n-gram overlap while improving semantic correctness.

A crucial nuance in interpreting the 16.1% accuracy figure: this represents approximately 60 correct formalizations out of 371 (compared to 50 for the baseline). If we assume the improved typecheck rate (45.2%) means roughly 168 out of 371 outputs typecheck, then the accuracy-conditioned-on-typechecking is 60/168 ≈ 0.36—substantially lower than the baseline's 0.57. This suggests that retrieval increases the quantity of type-correct outputs but may decrease their average quality, which is consistent with retrieval helping the model produce plausible-looking Lean that is often semantically wrong. The paper does not analyze this conditional accuracy pattern explicitly.

Distilled Backtranslation Results

Distilled backtranslation is evaluated on PROOFGPT-1.3B for autoformalization (Table 3, "Dist. backtrans." row). The method lifts the model from 0% accuracy (few-shot baseline) to 3.2% accuracy—approximately 12 correct formalizations out of 371. The typecheck rate increases from 5.9% to 19.4% (a 3.3× improvement), and the BLEU score increases from 8.1 to 10.7.

The 3.2% accuracy is notably higher than the PROOFGPT-6.7B few-shot baseline (0%), meaning that a 1.3B model with distilled backtranslation fine-tuning outperforms a 5× larger model with only few-shot prompting on formalization accuracy. However, the 3.2% figure is still far below Code-davinci-002's baseline (13.4%)—the teacher model that generated the synthetic training data is substantially more capable than the student.

The paper does not report a formalization accuracy for the Code-davinci-002 teacher model on the synthetic pairs used for training—only on the ProofNet test set. This means we cannot directly assess whether the student's 3.2% accuracy represents a reasonable distillation of the teacher's capability or a significant degradation.

Cross-Method Comparisons

The paper does not provide a single unified comparison table or plot that places all methods on a common cost axis. The results are spread across rows of Table 3 with different base models. The implicit ordering by accuracy is:

Code-davinci-002 + prompt retrieval: 16.1%
Code-davinci-002 few-shot: 13.4%
PROOFGPT-1.3B + distilled backtranslation: 3.2%
PROOFGPT-1.3B few-shot and PROOFGPT-6.7B few-shot: 0%

The paper does not report prompt retrieval applied to PROOFGPT models, nor distilled backtranslation applied to Code-davinci-002 (which would be impossible since Code-davinci-002 weights are not accessible for fine-tuning). It also does not report the combination of prompt retrieval and distilled backtranslation (e.g., fine-tuning on synthetic data, then using retrieval-augmented prompts at inference), which would test whether the two methods are complementary.

Qualitative Analysis (Section 5.3)

The paper presents four case studies that illuminate the quantitative results with concrete examples of success and failure:

Case Study 1 (success): Code-davinci-002 correctly formalizes an exercise about maximal ideals from Artin's Algebra, demonstrating knowledge of mathlib conventions—using the typeclass ideal R for ideals versus the predicate is_maximal for maximality, recognizing that ideals coerce to sets for ∉ notation, and correctly expressing "only maximal ideal" as ∀ (N : ideal R), is_maximal N → N = M. This illustrates the library-knowledge component: the model knows the specific mathlib representations for these algebraic concepts.

Case Study 2 (prompt retrieval fixes an error): For a group theory exercise (no group of order pq is simple), vanilla Code-davinci-002 uses the nonexistent identifier simple_group instead of the correct is_simple_group. The retrieval-augmented version correctly uses is_simple_group because one of the four retrieved mathlib statements explicitly contains that declaration. This is a concrete demonstration of retrieval addressing the library-knowledge bottleneck: the model's semantic understanding was correct (it knew the theorem involved simple groups), but its knowledge of mathlib's specific naming convention was wrong, and retrieval provided the missing information.

Case Study 3 (failure, both baseline and retrieval): For a linear algebra exercise about orthogonal complements, the model incorrectly declares the vector space structure as [vector_space K V] instead of the mathlib-correct [module K V], uses subspace V instead of submodule K V, and critically fails to include the implicit hypothesis that the space is an inner product space ([inner_product_space K V]) over ℝ or ℂ ([is_R_or_C K]). The paper frames this as an example of the "major challenge" of "reliably inferring implicit hypotheses"—the model doesn't realize that U.orthogonal only makes sense in an inner product space, not an arbitrary vector space. Retrieval does not fix this failure, suggesting that retrieved mathlib declarations containing the correct typeclass constraints are not sufficient for the model to perform the logical inference that those constraints must be added.

Case Study 4 (looping failure mode): PROOFGPT-6.7B generates a repetitive looping output like theorem nilpotent_of_nilpotent_of_nilpotent_of_nilpotent_of_nilpotent_of_nilpotent... when attempting to formalize a theorem about nilpotent elements. The paper connects this to the decoding pathology described by Holtzman et al. (2019): the likelihood of a repeated phrase increases with each repetition, and greedy decoding produces text with higher likelihood than natural text. The key diagnostic point is that "repetitive looping does not occur with Code-davinci-002, suggesting that the problem may disappear with scale"—but since many other differences exist between PROOFGPT and Code-davinci-002 besides parameter count, this is a correlation rather than a demonstrated causal relationship.

Ablation Studies and Robustness Checks

The paper contains several analyses that function as implicit ablations, though none are labeled as such:

Shot count for PROOFGPT vs. Code-davinci-002: The paper notes (Section 4.1.1, Appendix C) that PROOFGPT models receive 6-shot prompts while Code-davinci-002 receives 12-shot prompts, due to the 2,048 vs. 8,192 token context window difference. This is a confound: the 0% PROOFGPT accuracy could partially reflect having half as many examples rather than purely reflecting model capability. No ablation equalizing shot count (e.g., 6-shot Code-davinci-002 or using a larger-context PROOFGPT) is reported.

PROOFGPT scale comparison: The PROOFGPT results include both 1.3B and 6.7B parameter scales (Table 3). Counter to expectations, the larger model does not improve on any metric: accuracy remains 0% at both scales, typecheck rate drops slightly (5.9% → 4.3%), BLEU drops (8.1 → 4.7), and informalization compile rate drops (0.77% → 0.70%). The paper does not provide an explanation for this inverse scaling. The informalization accuracy does increase (4.3% → 6.5%), which is the only metric moving in the expected direction.

Prompt retrieval: k=4 fixed. The retrieval method uses k=4 nearest neighbors without ablating the number of retrieved examples. Larger k would provide more context but reduce space for other examples in the fixed-context prompt, while smaller k might miss relevant declarations. The sensitivity of results to k is not explored.

Prompt retrieval: embedding model fixed. All experiments use OpenAI's text-embedding-ada-002. No alternative embedding models (e.g., Codex embeddings, sentence transformers fine-tuned on mathematical text) are evaluated. The paper's finding that retrieval against $\hat{y}$ (coarse formalization) outperforms retrieval against $x$ (natural language) is reported from "preliminary experiments" without quantitative data.

Distilled backtranslation: teacher model fixed. Only Code-davinci-002 is used as the teacher. No ablation using a different teacher (e.g., GPT-3.5, a smaller open model, or the same PROOFGPT-1.3B as teacher) is reported. The paper cannot distinguish whether the 3.2% accuracy results from the teacher's quality specifically or from the backtranslation methodology generally.

Distilled backtranslation: student architecture ablation. The paper mentions (Appendix D) that "both the Pythia-1.4b and PROOFGPT-1.3B model are finetuned according to the hyperparameters above" for distilled backtranslation, but Table 3 reports only PROOFGPT-1.3B results. The Pythia-1.4B (base model without proof-pile fine-tuning) results are not shown, making it impossible to determine whether proof-pile pre-fine-tuning is necessary for backtranslation to work or whether the synthetic data alone would suffice.

Distilled backtranslation: data quantity ablation. All 90,530 mathlib theorems are used for synthetic data generation. No ablation varying the quantity of synthetic training data (e.g., 10K, 30K, 90K pairs) is reported, which would reveal whether performance continues to improve with more synthetic data or plateaus.

Checkpoint selection for backtranslation: The "minimum validation loss checkpoint, which occurs at 15,000 training steps" is used (Appendix D). No comparison to the final checkpoint (20,000 steps) is reported, leaving unclear whether validation loss correlates with formalization accuracy—a critical question given that the validation set presumably consists of held-out synthetic pairs, not real autoformalization examples.

Prompt format for retrieval: The retrieval-augmented prompt uses a 3-shot format, compared to 12-shot for the baseline (Appendix C). This means the 16.1% accuracy is achieved with one-quarter as many demonstration examples as the 13.4% baseline—a confound that complicates isolating the benefit of retrieval from the effect of shot count. A 3-shot baseline without retrieval is not reported.

Critical Assessment

Do the experiments support the claim that ProofNet is a benchmark that will "drive progress in autoformalization and automatic theorem proving" (Abstract, Section 1)?

The experiments establish that ProofNet is non-trivially difficult but not impossibly hard for current systems. The best method achieves 16.1% accuracy with substantial room for improvement. This is the sweet spot for a benchmark: it discriminates between methods (prompt retrieval improves over baseline, distilled backtranslation improves over PROOFGPT few-shot) and leaves headroom for future progress. However, the paper evaluates only statement autoformalization—it explicitly defers formal theorem proving and proof autoformalization to future work (Section 4). So the claim that ProofNet supports automatic theorem proving is aspirational; the experiments demonstrate only its utility for autoformalization evaluation.

A more significant limitation is that the benchmark's difficulty may be partially driven by the specific implementation quirks of mathlib rather than by general autoformalization capability. Case Studies 1 and 2 show that knowing whether maximality is expressed as a typeclass or a predicate (is_maximal vs. an ideal type), or whether simple groups use simple_group or is_simple_group, is memorization of mathlib conventions rather than mathematical understanding. A model could be an excellent mathematical reasoner with poor knowledge of mathlib's naming choices and score poorly on ProofNet; conversely, a model fine-tuned extensively on mathlib could memorize these conventions without deep mathematical understanding. The benchmark conflates these two capabilities, which is a legitimate design choice (real autoformalization requires both) but limits what conclusions can be drawn from performance improvements—does a higher score mean better math, or better mathlib memorization?

The paper partially addresses this concern through the stylistic choice to favor "applying general results to specific cases" over abstract theory-building (Section 2), but this only partially mitigates the problem—applying Sylow theorems to |G| = 312 still requires knowing what mathlib calls its Sylow theorem lemma.

Do the experiments support the claim that prompt retrieval and distilled backtranslation "outperform our few-shot baselines" (Abstract, Section 1)?

Prompt retrieval: The 16.1% vs. 13.4% improvement is real but the magnitude (+2.7 percentage points) is modest compared to the baseline's performance level. The near-doubling of typecheck rate (23.7% → 45.2%) is more impressive and likely more robust. However, the retrieval method is confounded with shot count (3-shot retrieval vs. 12-shot baseline), making the accuracy comparison ambiguous—we cannot determine how much of the improvement comes from retrieval specifically versus the change in prompt format. A proper comparison would match shot counts between conditions. Furthermore, the retrieval method is only evaluated on Code-davinci-002; we don't know whether it generalizes to other models or whether it is specific to that model's ability to leverage retrieved declarations. The paper's abstraction that retrieval "outperforms" the baseline is fair given the data, but the margin is small and the statistical significance unknown.

Distilled backtranslation: The 3.2% vs. 0% (PROOFGPT-1.3B few-shot) improvement is directionally clear—backtranslation demonstrably provides a training signal that few-shot prompting does not at this model scale. But the absolute performance (3.2%) is very low, and the comparison against the PROOFGPT-6.7B few-shot baseline (also 0%) is not informative—a 1.3B model with backtranslation surpassing a 6.7B model at 0% tells us more about how poor the few-shot baseline is than about how good backtranslation is. The more meaningful comparison would be: how does the backtranslation-trained 1.3B model compare to direct fine-tuning on ProofNet's training data (if a split were created) or to the teacher model's performance on synthetic pairs? Neither comparison is provided. The claim that backtranslation "outperforms" the baseline is technically true but masks that "outperform" means 3.2% vs. 0%—both are very low, and the method has not been shown to approach practical utility.

Do the experiments support the claim that "large pre-trained language models have a strong grasp of the semantics of formal mathematics, and primarily struggle with generating lexically correct and type correct Lean code" (Section 5.1)?

This is the most interesting and best-supported interpretive claim in the paper. The evidence is:

Code-davinci-002 achieves 62.3% informalization accuracy—when given formal Lean code, it can correctly explain what the theorem says in natural language at a rate nearly 5× higher than it can formalize in the reverse direction. This shows the model understands formal mathematics when reading it.
The ratio of accuracy to typecheck rate for formalization is approximately 0.57—conditional on generating valid Lean, the model is correct more than half the time. This suggests the bottleneck is producing valid syntax, not understanding what to say.
Prompt retrieval disproportionately improves typecheck rate (+21.5 points) relative to accuracy (+2.7 points), suggesting it helps with the syntactic/lexical dimension more than the semantic dimension.

However, "strong grasp" is an overstatement for a system that gets 62.3% informalization accuracy—it fails on 37.7% of problems even in the easier direction. And the claim is only tested on Code-davinci-002; PROOFGPT models achieve 4.3–6.5% informalization accuracy, which does not support a claim of "strong grasp." The generalization is therefore specific to very large, code-trained models, not to language models generally.

A deeper concern: the 62.3% informalization accuracy might partially reflect the ease of the specific informalization task rather than deep semantic understanding. If the formal statement contains the keyword is_simple_group and the model generates "G is not a simple group," that's correct but doesn't require understanding the definition of simple groups—it could be largely lexical translation of identifiers. The paper doesn't analyze the complexity of correct vs. incorrect informalizations to distinguish shallow lexical translation from deep semantic understanding.

Genuine weaknesses in the experimental design

No statistical significance reporting. The test set is 371 examples. A 2.7 percentage point improvement (13.4% → 16.1%) corresponds to 10 additional correct formalizations (50 → 60). Without confidence intervals or significance tests, we cannot rule out that this difference is within the range of sampling variability, especially given that the few-shot baseline accuracy is itself sensitive to the specific choice of 12 examples and their ordering. The paper acknowledges that "few-shot learning performance is highly sensitive to the exact prompt that is used" (Section 4.1.2) but does not evaluate this sensitivity empirically by varying the prompt.

Single evaluation of few-shot prompts. Each model is evaluated with a single fixed prompt (12-shot for Codex, 6-shot for PROOFGPT). Given the known prompt sensitivity, a proper baseline would report mean and variance over multiple prompt configurations (different random selections of examples, different orderings). The paper's own prompt retrieval method is motivated by this sensitivity, yet the baseline's sensitivity is never quantified.

No PROOFGPT + prompt retrieval. The retrieval method is only tested on Code-davinci-002. Testing it on PROOFGPT would reveal whether the retrieval benefit is model-dependent and whether smaller models can leverage retrieved context as effectively as large models.

No combination of prompt retrieval and distilled backtranslation. These are presented as independent methods improving over the baseline, but they operate at different stages (inference-time vs. training-time). A natural experiment—fine-tune PROOFGPT-1.3B with backtranslation, then use retrieval-augmented prompts at inference—is not reported. This would test whether the gains are additive or redundant.

The expert evaluation process is not described. The paper states that autoformalizations are "evaluated for correctness by a human expert" (Section 4.1.1) but provides no details on: how many experts performed the evaluation, whether inter-annotator agreement was measured, what specific criteria were used to judge semantic equivalence, whether evaluators were blind to which method generated each output, or how edge cases (formally correct but inelegant, semantically equivalent but structurally different) were handled. This makes the accuracy numbers difficult to interpret and impossible to replicate. The reported accuracies could be biased by evaluator expectations or inconsistent standards.

No training set for ProofNet. All 371 examples are used for testing. This is appropriate for evaluating in-context learning and externally-trained models, but it means ProofNet cannot be used for supervised fine-tuning experiments without creating a custom split—limiting its utility for a major class of methods that future work might explore.

Teacher-student capability gap is not characterized. For distilled backtranslation, we know the teacher (Code-davinci-002) achieves 13.4% on the real ProofNet test set, but we don't know its performance on the synthetic training pairs it generates. If the teacher's synthetic informalizations are poor quality, the student's 3.2% accuracy might represent a ceiling imposed by training data quality rather than the student's capacity. Quantity of training data (90,530 pairs) is reported but not quality.

Missing experiments that would strengthen the paper

Multi-prompt baseline: Evaluate few-shot Code-davinci-002 with 3–5 different randomly-sampled prompt configurations and report mean ± standard deviation, establishing the baseline's sensitivity range.
Shot-count-matched retrieval baseline: Compare 3-shot + retrieval against 3-shot without retrieval (and ideally 12-shot without retrieval against 12-shot + retrieval in a larger-context model) to isolate the retrieval benefit.
Retrieval method applied to PROOFGPT: Test whether smaller models benefit from retrieval as much as large models, which would inform the generality of the method.
Teacher quality ablation for backtranslation: Use a weaker teacher (e.g., PROOFGPT-6.7B with few-shot informalization) to generate synthetic data and measure how student performance degrades, characterizing the dependency on teacher quality.
Backtranslation training data quantity sweep: Train with 10K, 30K, 60K, 90K synthetic pairs to determine whether more data continues to help or whether performance saturates.
Benchmarking on mathlib-held-out data: Create a split of ProofNet or a held-out set of mathlib theorems to test whether models are memorizing mathlib patterns or generalizing.

Where the claims hold conditionally

The claim that prompt retrieval improves autoformalization (Abstract: "outperform our few-shot baselines") holds for Code-davinci-002 specifically, with a 3-shot retrieval prompt compared to a 12-shot baseline—this is a conditional improvement with confounded experimental conditions and unknown statistical significance. The claim has not been demonstrated for any other model.

The claim that distilled backtranslation improves performance (Abstract: "outperform our few-shot baselines") holds for PROOFGPT-1.3B specifically, lifting accuracy from 0% to 3.2%. This is technically true but the absolute performance is very low and the method has not been shown to scale to higher accuracies or larger models. The claim that it "outperforms" is accurate in direction but the magnitude is small enough that practical significance is questionable.

The paper's broader implicit claim—that ProofNet enables systematic progress measurement in autoformalization—is supported by the experiments to the extent that (1) the benchmark discriminates between methods, (2) the metrics are interpretable (with the typecheck rate recommendation), and (3) the qualitative case studies illuminate specific failure modes. However, the lack of statistical rigor, the single-model evaluation of the best methods, and the absence of training data limit the benchmark's immediate utility for the community. The paper successfully establishes that autoformalization is hard and that these methods help modestly; it does not establish by how much with the precision needed for fine-grained progress tracking.

6. Limitations and Trade-offs

6.1 ProofNet Tests Only Statement Autoformalization, Not the Full Autoformalization Pipeline

The assumption or constraint. The paper explicitly restricts its empirical evaluation to statement autoformalization (informal theorem statement → formal theorem statement) and its inverse (informalization). The Introduction and Abstract position ProofNet as a benchmark for both "autoformalization and formal proving," and Section 2 lists four supported tasks including formal theorem proving and proof autoformalization. However, Section 4 states:

"Due to the engineering challenges of implementing neural theorem proving systems in Lean, we leave an investigation of formal theorem proving and proof autoformalization to future work."

The paper evaluates zero of the four tasks that involve proof generation. The benchmark's parallel data structure—informal statement, informal proof, formal statement—is designed to support evaluation of proof autoformalization (generating a formal proof given an informal statement, informal proof, and formal statement), but no baseline results are reported for this task.

The consequence. A practitioner evaluating whether ProofNet can guide autoformalization system development must recognize that the paper demonstrates utility for only the easiest sub-task in the pipeline. Statement autoformalization tests whether a model can map mathematical concepts to their mathlib representations—it does not test whether a model can generate a correct formal proof, which requires step-by-step logical reasoning, tactic selection, and lemma application within Lean's tactic framework. The gap between statement formalization (13.4–16.1% for Code-davinci-002) and proof formalization is almost certainly large—formal proof generation is a substantially harder problem that miniF2F (Zheng et al., 2022) addresses, and ProofNet's evaluations provide no signal about performance on this harder task. An autoformalization system that perfectly formalizes statements but cannot prove them would be useless for the paper's motivating vision of "extracting a training signal from vast corpora of natural language mathematics data" (Section 1).

What evidence exists in the paper. The paper contains zero experimental results on formal theorem proving or proof autoformalization. The task descriptions in Section 2 and the benchmark structure are the only indicators of intended future use. There is no discussion of what formal proof evaluation would require (e.g., a Lean evaluation harness, pass@k metrics, compute budget for proof search), nor any estimate of the difficulty gap between statement and proof autoformalization.

Mitigation status. The paper acknowledges this limitation by explicitly deferring proof-related tasks "to future work" (Section 4). It does not attempt to bound the difficulty gap, provide infrastructure for proof evaluation (beyond including informal proofs in the dataset), or report any preliminary proof-generation results. The limitation is transparently stated but entirely unresolved—ProofNet is, for now, exclusively a statement autoformalization benchmark with proof evaluation as an aspiration.

6.2 Difficulty Estimation Is Not Practical: Expert Human Evaluation Does Not Scale

The assumption or constraint. The gold-standard autoformalization metric is expert human judgment of semantic correctness, because:

"there is no general way to automatically verify whether two statements that are not definitionally equal have the same mathematical content" (Section 4.1.1).

The paper employs human experts proficient in Lean to evaluate every generated formalization against the ground-truth formal statement in ProofNet. The typecheck rate is proposed as a cheaper proxy metric (Section 5.2), and the paper recommends it "be used as a predictor of autoformalization performance when evaluating accuracy is too costly." However, the paper provides no automated metric that reliably tracks semantic correctness—typecheck rate only correlates with accuracy at roughly 0.5:1 (half of type-correct generations are semantically correct), and BLEU is shown to be anti-correlated with accuracy in regimes where methods improve (prompt retrieval increases accuracy while decreasing BLEU by over 10 points, Table 3).

The consequence. Autoformalization research using ProofNet faces a fundamental evaluation bottleneck. Every new method, hyperparameter configuration, prompt variation, or model checkpoint requires an expert human evaluator to judge hundreds of generated formalizations. This is slow, expensive, and limits the pace of iteration that the benchmark can support. The paper's own experimental design reflects this constraint: there are no ablations varying prompt format, multi-seed evaluation, or hyperparameter sweeps—likely because each additional experiment would require another round of costly human evaluation. The typecheck rate proxy partially alleviates this for coarse progress tracking, but the 0.5:1 accuracy-to-typecheck ratio means large changes in typecheck rate can correspond to small or zero changes in accuracy (as with prompt retrieval's +21.5 typecheck points yielding only +2.7 accuracy points), making it unreliable for fine-grained method comparison.

Furthermore, the absence of inter-annotator agreement metrics, evaluation rubrics, or blinding protocols (Section 5, Critical Assessment) means the reported accuracies may not be reproducible by other researchers with different expert evaluators or different semantic equivalence standards. This undermines ProofNet's function as a standardized benchmark: if two research groups report accuracy on ProofNet, differences could reflect evaluator disagreement rather than genuine method improvement.

What evidence exists in the paper. Table 3 reports the three metrics (accuracy, typecheck rate, BLEU) side-by-side, and Section 5.2 discusses their correlations. The prompt retrieval case (accuracy ↑, BLEU ↓) is the clearest evidence that automatic surface-form metrics are misleading. The paper does not report: inter-annotator agreement, evaluation time per example, number of evaluators, or any attempt to develop an automated semantic equivalence metric (e.g., by testing whether the generated formal statement is provably equivalent to the ground truth in Lean, though this would require proof automation that the paper notes is unavailable for Lean).

Mitigation status. The paper partially addresses this by recommending typecheck rate as a practical proxy. It does not attempt to develop an automated evaluation metric, train an equivalence classifier, or characterize the cost and reliability of the human evaluation process. The limitation is acknowledged but not resolved—it is presented as a feature of the problem domain (formal statements can be semantically equivalent without being syntactically identical) rather than a gap to be addressed. Future work on ProofNet-based research will either need to accept the evaluation bottleneck or develop automated metrics that correlate better with expert judgment than typecheck rate does.

6.3 Single Benchmark, Single Formal System, Single Model Family for Strong Results

The assumption or constraint. The paper's strongest experimental results—few-shot autoformalization at 13.4%, prompt retrieval at 16.1%—are obtained exclusively with Code-davinci-002 via the OpenAI API. The PROOFGPT models achieve 0% few-shot accuracy, making Code-davinci-002 the only model family demonstrating non-trivial performance. All formalizations target Lean 3 with mathlib specifically. All problems are drawn from undergraduate pure mathematics textbooks in four areas (analysis, linear algebra, abstract algebra, topology) with a small number from the Putnam Competition. The paper does not evaluate on any other ITP (Isabelle, Coq, Metamath), any other formal library, any other mathematical domain (applied mathematics, probability, combinatorics beyond what textbook exercises cover), or any other model family besides Code-davinci-002 and PROOFGPT.

The consequence. Three distinct generalization uncertainties arise, none addressed by the paper:

Model dependence: The 13.4–16.1% accuracy figures may be specific to Code-davinci-002's training data, architecture, or scale. Code-davinci-002 was trained on a large corpus including GitHub code (Chen et al., 2021), which likely includes Lean and mathlib source files. Its performance may partially reflect memorization of mathlib content seen during pretraining rather than generalizable autoformalization capability. Without evaluating multiple model families (GPT-3.5, Claude, open-source models at comparable scales), we cannot distinguish Code-davinci-002-specific effects from general autoformalization difficulty. A practitioner choosing a model for autoformalization receives guidance about exactly one proprietary model.
ITP/library dependence: Lean 3's dependent type theory imposes specific constraints (typeclass resolution, implicit arguments, coercion rules) that differ from Isabelle/HOL (used by Wu et al., 2022a) or Metamath (used by Polu and Sutskever, 2020). The difficulty of autoformalization may be partially determined by how "natural" a formal system's syntax is relative to mathematical natural language. ProofNet's difficulty estimates cannot be transferred to other ITPs without building parallel benchmarks.
Domain dependence: Undergraduate pure mathematics exercises may systematically differ from other mathematical text. Research-level mathematics involves more complex, nested definitions and less standardized problem structures. Applied mathematics problems (optimization, differential equations, statistics) use different vocabulary and reasoning patterns. The paper's claim that ProofNet tests "reasoning over the core of an undergraduate mathematics" (Section 1) is accurate, but it does not test reasoning over applied mathematics, geometry, combinatorics, or any domain the authors explicitly excluded due to "less mature" mathlib support (Section 2).

What evidence exists in the paper. The paper transparently reports that all strong results come from Code-davinci-002 (Table 3) and that the benchmark is Lean 3 / mathlib-specific (Section 2). It acknowledges that PROOFGPT is "inferior to the Minerva models" (Section 3) and does not claim the results generalize. The problem sources are listed in Appendix B, confirming the pure-mathematics focus. The paper provides no cross-model, cross-ITP, or cross-domain evaluation.

Mitigation status. The paper does not attempt to mitigate these generalization uncertainties. It does not evaluate any model besides Code-davinci-002 and PROOFGPT, any ITP besides Lean 3, or any domain outside undergraduate pure mathematics. The authors frame ProofNet as a specific benchmark for a specific capability (Lean 3 formalization of undergraduate mathematics) and do not claim broader coverage. However, the Introduction and Abstract use language suggesting broader implications ("autoformalization and automatic theorem proving" without qualification), creating a tension between the paper's framing and its experimental scope. A practitioner should treat the reported results as specific to (Code-davinci-002, Lean 3, undergraduate pure math) until demonstrated otherwise.

6.4 Difficulty Estimation Cost Is Not Accounted for—Prompt Retrieval Doubles the API Calls per Problem

The assumption or constraint. The prompt retrieval method (Section 4.1.2) uses a two-stage pipeline: an initial few-shot generation to produce a coarse formalization \hat{y}, followed by embedding-based retrieval of k=4 nearest-neighbor mathlib declarations, then a second few-shot generation with the retrieval-augmented prompt. The paper reports this method's accuracy (16.1%) and typecheck rate (45.2%) in Table 3, but does not account for the doubled inference cost in any metric. The retrieval step itself (generating \hat{y}) consumes one full Code-davinci-002 API call; the augmented generation consumes a second. Embedding generation via text-embedding-ada-002 and nearest-neighbor search add further (smaller) costs.

The consequence. The 16.1% accuracy is achieved with twice the inference budget of the 13.4% baseline (two generations per problem vs. one). A fair comparison would either (a) report baseline performance at 2× the generation budget (e.g., by sampling two independent few-shot generations and selecting the best, or by using a larger budget per generation) or (b) report retrieval performance normalized by inference cost. Without this accounting, we cannot determine whether the retrieval benefit is due to the retrieval mechanism specifically or simply due to using more computation. The 2.7 percentage point accuracy gain (13.4% → 16.1%) could potentially be matched or exceeded by simpler methods with equivalent compute—for instance, generating multiple few-shot samples and selecting the one with highest typecheck probability, or using majority voting across multiple generations.

The paper's claimed 4× efficiency gain from compute-optimal scaling (reference example) has no analog here; the retrieval method's cost multiplier is neither measured, reported, nor discussed. This is particularly significant because prompt retrieval's primary benefit—the near-doubling of typecheck rate—might be achievable through simpler, cheaper interventions (e.g., temperature tuning, rejection sampling against the typechecker) that don't require a full second API call.

What evidence exists in the paper. The two-stage nature of prompt retrieval is described in Section 4.1.2. The paper does not report: the number of API calls per problem for retrieval vs. baseline, the total inference cost in tokens or dollars, the latency impact of the two-stage pipeline, or any cost-controlled comparison (e.g., 2× generation budget baseline). The paper does not acknowledge this cost disparity as a confound in interpreting the retrieval results.

Mitigation status. Not addressed. The paper treats prompt retrieval as a method-level contribution and compares its output quality to the baseline without normalizing for computational cost. This is a standard practice in prompt engineering literature, but it means the headline comparison (16.1% vs. 13.4%) is not on equal footing. A cost-aware practitioner should interpret retrieval's benefit as an upper bound—the true per-unit-compute improvement may be smaller or zero.

6.5 No Training Split—ProofNet Cannot Be Used for Supervised Fine-Tuning Experiments

The assumption or constraint. ProofNet consists of 371 examples, all used as an evaluation test set. The paper does not define a training/validation/test split. Section 2 describes the dataset as a "benchmark" for evaluation. All reported experiments use either in-context learning (no ProofNet training data) or external synthetic data generation (distilled backtranslation using mathlib theorems, not ProofNet examples). The paper mentions no mechanism for using ProofNet examples as training data.

The consequence. A major class of potential autoformalization methods—supervised fine-tuning on real parallel data—cannot be evaluated using ProofNet as released. Researchers who want to fine-tune a model on (informal, formal) pairs must either: (a) create their own split of ProofNet, reducing an already-small test set (371 examples) and making cross-paper comparisons impossible since different groups will use different splits; or (b) find or create another parallel dataset, defeating the purpose of a standardized benchmark. This limitation is structural: with 371 total examples and five difficulty areas, a reasonable train/test split (e.g., 80/20) would leave only ~74 test examples (~15 per subject area), making accuracy estimates noisy. Yet without any training split, ProofNet cannot measure progress from the most straightforward approach to improving autoformalization—collecting more human-annotated parallel data and fine-tuning on it.

This is particularly consequential given the paper's own results: distilled backtranslation achieves only 3.2% accuracy using synthetic data, and the few-shot baseline achieves 13.4%. The natural next question—"what accuracy could be achieved by fine-tuning on a few hundred real parallel examples?"—cannot be answered using ProofNet as currently structured. The benchmark's design choice to use all data for testing implicitly assumes that in-context learning or external synthetic data are the only viable approaches, which may prematurely foreclose supervised methods.

What evidence exists in the paper. The paper describes the full 371 examples as the benchmark (Section 2) with no mention of splits. All evaluations use the full set as a test set. The paper does not discuss the training split issue, the minimum dataset size needed for meaningful accuracy comparisons, or plans for a future release with defined splits.

Mitigation status. Not addressed. The paper does not acknowledge the absence of a training split as a limitation. From the authors' perspective, ProofNet is an evaluation-only benchmark (analogous to miniF2F's test set), and training data is expected to come from external sources (mathlib, proof-pile, synthetic generation). However, the existence of only 371 real parallel examples in the world (ProofNet itself) makes the inability to use those examples for training a significant practical constraint. Future work could create an official split or expand the dataset to enable both training and evaluation, but neither is proposed in the paper.

6.6 The 0% PROOFGPT Baseline Obscures Whether Small Models Can Autoformalize at All

The assumption or constraint. The PROOFGPT models achieve 0% few-shot autoformalization accuracy at both 1.3B and 6.7B scales (Table 3). The paper attributes this to parameter count ("likely owing to their smaller parameter count," Section 5.1) and uses it as motivation for distilled backtranslation, which lifts PROOFGPT-1.3B to 3.2%. However, the PROOFGPT few-shot baseline uses 6-shot prompts (vs. Code-davinci-002's 12-shot) due to the 2,048-token context window (Section 4.1.1, Appendix C), and the paper does not test PROOFGPT with prompt retrieval, which was the most effective method for improving typecheck rate on Code-davinci-002.

The consequence. The 0% accuracy ceiling for PROOFGPT few-shot is multiply confounded: smaller model, fewer shots, no retrieval augmentation, and no reported decoding parameter optimization. We cannot determine whether the 0% reflects a fundamental capability floor (models below a certain scale genuinely cannot autoformalize at all) or an experimental design choice (insufficient prompting, suboptimal decoding). The paper's claim that 0% is "likely owing to smaller parameter count" is speculative—Code-davinci-002's parameter count is not public, and the 6-shot vs. 12-shot difference alone could account for some or all of the gap. Without a 12-shot PROOFGPT baseline (using a larger-context model or truncation) or a 6-shot Code-davinci-002 ablation, the effect of shot count vs. model scale is unidentified.

This matters for the paper's narrative about distilled backtranslation. The 3.2% accuracy achieved by backtranslation-trained PROOFGPT-1.3B is compared against a 0% few-shot baseline, making the improvement appear dramatic. But if a better-prompted PROOFGPT baseline achieved even 1–2%, the backtranslation improvement would be smaller and the method's value proposition weaker. The paper cannot rule out that simple prompt engineering (more shots, better example selection, retrieval) on PROOFGPT would match or exceed 3.2% without any fine-tuning.

What evidence exists in the paper. Table 3 reports 0% for both PROOFGPT scales with 6-shot prompts. The 6-shot vs. 12-shot discrepancy is noted in Section 4.1.1 and Appendix C. The paper does not report: PROOFGPT with 12-shot prompts (requiring a context window extension or output truncation strategy), PROOFGPT with prompt retrieval, Code-davinci-002 with 6-shot prompts, or any decoding parameter sweep for PROOFGPT. The PROOFGPT informalization results (4.3% at 1.3B, 6.5% at 6.7B) demonstrate that these models have non-zero capability in the easier informalization direction, suggesting the 0% formalization floor may not be absolute.

Mitigation status. Partially acknowledged by reporting the 6-shot constraint, but not experimentally addressed. The paper's focus on Code-davinci-002 for strong results and PROOFGPT only as a substrate for backtranslation means the 0% baseline is treated as a given rather than as a finding to be investigated. A practitioner considering whether to use small open-source models for autoformalization should treat the 0% figure as a lower bound (achievable with 6-shot prompting and default decoding) rather than a capability ceiling—better prompting or retrieval might yield non-zero performance, but the paper provides no evidence either way.

7. Implications and Future Directions

How This Work Changes the Landscape

ProofNet shifts the autoformalization research landscape by providing the first standardized, reproducible benchmark for a task that previously lacked any shared evaluation framework. Prior to ProofNet, autoformalization was evaluated in ad-hoc fashion—Wu et al. (2022a) tested on hand-selected Isabelle examples, Jiang et al. (2022b) demonstrated proof autoformalization with infrastructure dependencies specific to Isabelle/HOL, and each paper effectively defined its own test set. There was no way to compare methods across papers, track progress over time, or diagnose failure modes systematically. ProofNet provides that missing infrastructure: 371 parallel (informal statement, informal proof, formal statement) triples in Lean 3, openly available, with clear evaluation protocols (though human-judged, making them expensive). This alone is an infrastructure-level contribution that enables a field to form around a shared measurement target—analogous to how ImageNet enabled systematic progress in computer vision, or how miniF2F (Zheng et al., 2022) standardized evaluation for formal theorem proving.

But the paper's deeper reframing is that autoformalization difficulty is not primarily about reasoning depth (the dimension stressed by olympiad benchmarks like miniF2F and MATH) but about library-knowledge breadth. The Figure 1 comparison between a mathlib-style abstract theorem and a ProofNet-style concrete application problem (a group of order 312 has a normal Sylow subgroup) makes this distinction explicit: the challenge is recognizing which general results apply and correctly navigating mathlib's naming conventions, typeclass structures, and representational choices—not constructing a multi-step deductive chain from elementary axioms. The case studies in Section 5.3 provide granular evidence: Code-davinci-002 succeeds at logical reasoning (correctly expressing "only maximal ideal" as a universal quantification) but fails at library conventions (using simple_group instead of is_simple_group). This reframing matters because it redirects research investment: if autoformalization is bottlenecked by library knowledge rather than reasoning, then progress requires better premise retrieval, larger-context models that can ingest relevant documentation, and training objectives that incentivize correct identifier selection—not primarily better chain-of-thought reasoning or proof search architectures.

The paper also resolves a latent tension in the autoformalization literature. Prior work had demonstrated that large language models can autoformalize (Wu et al., 2022a showed in-context autoformalization in Isabelle) but with unknown reliability and unclear failure modes. ProofNet's quantitative results and qualitative case studies provide the first systematic characterization of where current models succeed and fail: they have strong semantic understanding of formal mathematics (62.3% informalization accuracy for Code-davinci-002) but struggle to produce syntactically valid Lean code (23.7% typecheck rate), and the bottleneck is library conventions and implicit hypothesis inference (Case Studies 1–3) rather than fundamental mathematical misunderstanding. This creates a clear research agenda: the problem to solve is not "making models understand mathematics" (they already do, to a non-trivial degree) but "making models produce correct mathlib code"—a more tractable framing that suggests specific interventions (retrieval augmentation, fine-tuning on library documentation, typechecker-guided decoding).

The paper also establishes that autoformalization is viable with purely synthetic training data, though at low absolute performance. The distilled backtranslation result—PROOFGPT-1.3B achieves 3.2% accuracy after fine-tuning exclusively on synthetic pairs generated by Code-davinci-002—demonstrates that the complete absence of parallel corpora is not an absolute blocker for supervised approaches. This is a proof of concept rather than a practical solution, but it changes the conversation from "we cannot train autoformalization models because we lack parallel data" to "we can train weak autoformalization models with synthetic data; how do we make them stronger?" The authors themselves express ambivalence about backtranslation as a long-term strategy, predicting that in-context learning will become "unreasonably effective" at sufficient scale (Section 6), but the result provides a concrete baseline that future work can improve through better teacher models, larger student models, or more sophisticated synthetic data generation.

Finally, the paper's analysis of evaluation metrics (Section 5.2) provides a methodological correction for the field. BLEU—the default automatic metric in sequence-to-sequence tasks—is shown to be anti-correlated with accuracy in the prompt retrieval setting (accuracy increases +2.7 points while BLEU drops −10.3 points). This is not a weak correlation; it is a directionally wrong signal that would cause a BLEU-optimizing researcher to reject a beneficial method. The paper's recommendation to use typecheck rate as the primary automatic proxy, with expert judgment for final validation, provides a practical evaluation protocol that balances cost and reliability. This is an incremental but important contribution: without a cheap, reliable progress indicator, benchmark-driven research stalls between expensive human-evaluation rounds.

Follow-Up Research This Work Enables

Developing automated semantic equivalence metrics for autoformalization. The paper's central evaluation bottleneck is that only human experts can reliably judge whether a generated formal statement is semantically equivalent to the ground truth. The typecheck rate proxy correlates only moderately (accuracy/typecheck ≈ 0.5 for Code-davinci-002). A strong follow-up would develop and validate an automated semantic equivalence metric, potentially by: (a) using Lean's kernel to check whether the generated statement is definitionally equal to the ground truth (which is too strict but provides a lower bound), (b) training a classifier on (generated, ground-truth) pairs labeled by expert judgment to predict equivalence, or (c) automatically testing equivalence by attempting to prove each statement from the other using a bounded proof search. The evaluation would report correlation with expert judgments on ProofNet's 371 examples and measure whether the metric preserves the ranking between methods (does it correctly identify that prompt retrieval improves over baseline?). If successful, this would eliminate the human-evaluation bottleneck that currently limits ProofNet's utility for rapid iteration.

Prompt retrieval applied to open-source models at scale, with cost-controlled comparison. The paper's prompt retrieval method is evaluated only on Code-davinci-002, a proprietary model, and its accuracy improvement (+2.7 points) is confounded with shot count (3-shot retrieval vs. 12-shot baseline) and inference cost (2× the API calls per problem). A strong follow-up would: (a) evaluate prompt retrieval on a range of open-source models (LLaMA-2, Mistral, DeepSeek-Coder at 7B–70B scales) to determine whether the retrieval benefit generalizes across model families and scales, (b) perform a properly cost-controlled comparison by running retrieval at equivalent total inference budget to the baseline (e.g., 2× baseline generations with majority voting vs. retrieval with one generation), and (c) ablate retrieval parameters (number of retrieved neighbors k, embedding model choice, retrieval against natural language vs. coarse formalization with quantitative data). This would establish whether retrieval is a genuinely superior allocation of inference compute, or whether its benefits can be matched by simpler, cheaper interventions.

Fine-tuning on ProofNet with a proper train/test split to establish supervised performance ceilings. ProofNet currently has no training split, preventing supervised fine-tuning experiments on real parallel data. A natural follow-up would: (a) create an official training split (e.g., 250 training, 60 validation, 61 test, ideally stratified by subject area and difficulty), (b) fine-tune a range of base models (CodeLlama, DeepSeek-Coder, LLaMA) on the training examples with varying dataset sizes to characterize the sample efficiency curve—how many real parallel examples are needed to surpass the 13.4% few-shot Code-davinci-002 baseline, and whether performance saturates at ProofNet's scale or continues to improve. This would establish an empirical upper bound on what supervised approaches can achieve with ProofNet-scale data and determine whether collecting more parallel annotations (expanding ProofNet) is likely to yield further gains. The paper's distilled backtranslation result (3.2%) provides a lower bound; supervised fine-tuning on real data would provide an upper bound, and the gap between them would characterize the cost of synthetic data for this task.

Testing whether the typecheck rate bottleneck can be addressed through typechecker-guided decoding. The paper identifies that roughly half of Code-davinci-002's type-correct generations are semantically correct (0.57 accuracy/typecheck ratio), implying that increasing the proportion of type-correct outputs would directly improve accuracy. A concrete experiment: use rejection sampling where the model generates N candidates per problem and the first candidate that passes the Lean typechecker is returned (or the highest-likelihood type-correct candidate among a budget B). Measure accuracy as a function of the sampling budget N and compare to the baseline single-generation accuracy. This tests whether the primary bottleneck is generating any type-correct output (which sampling can address) versus generating a semantically correct output (which requires model capability). If accuracy scales well with sampling budget, this provides a practical deployment strategy; if it plateaus quickly, it confirms that the model's type-correct outputs are often semantically wrong in systematic ways, pointing toward fine-tuning on type-correct-but-wrong examples.

Expanding the benchmark to proof autoformalization with a Lean evaluation harness. The paper explicitly defers proof autoformalization and formal theorem proving to future work (Section 4). A natural extension would: (a) build a Lean evaluation harness that takes a formal statement and a generated formal proof attempt, runs the proof through Lean, and reports success/failure (this is deterministic and automatic, unlike statement equivalence, because Lean can automatically verify proofs), (b) establish baselines for proof autoformalization on ProofNet's 371 examples by providing the informal statement, informal proof, and formal statement (all present in the dataset) as input to a model and asking it to generate a formal proof, and (c) measure whether access to the informal proof improves formal proof success rates over generating a formal proof from the formal statement alone. This would connect ProofNet to the formal theorem proving literature (miniF2F, LeanDojo) and test the paper's motivating vision of extracting training signal from informal proofs.

Systematically characterizing whether autoformalization performance depends on domain-specific library maturity. The paper's problem selection criteria explicitly exclude areas where mathlib is "relatively less mature" (Euclidean geometry, combinatorics). A diagnostic follow-up would deliberately include a small number of problems from these excluded domains and measure whether performance degrades relative to well-supported domains (algebra, analysis), controlling for problem difficulty. This would quantify the dependence of autoformalization performance on library completeness—a crucial practical question for deciding when to deploy autoformalization systems on new mathematical domains. If performance is strongly library-dependent, this argues for investing in library formalization as a prerequisite for autoformalization; if models can generalize across library completeness levels (perhaps by inferring missing definitions from context), this suggests autoformalization may be more robust than the paper's design choices imply.

Practical Applications and Downstream Use Cases

Benchmarking and model selection for autoformalization components in larger systems. A research group building a system that combines neural theorem proving with autoformalization (e.g., to formalize a corpus of informal mathematical text and then prove theorems over the formalized library) needs to choose a base model for the autoformalization step. ProofNet provides a standardized evaluation: the group can test candidate models (Code-davinci-002, Claude, GPT-4, fine-tuned open-source models) on the 371-example benchmark, measure autoformalization accuracy and typecheck rate, and select the model that best balances accuracy and inference cost for their specific domain. The paper's finding that prompt retrieval nearly doubles typecheck rate (23.7% → 45.2%) for a 2× inference cost provides a concrete cost-accuracy tradeoff curve that can inform deployment decisions. The typecheck rate recommendation (Section 5.2) enables ongoing monitoring of autoformalization quality without continuous expensive human evaluation.

Curriculum design for training formal mathematics students on Lean. ProofNet's 371 examples span the undergraduate pure mathematics curriculum and are explicitly selected to involve "applying general results to specific cases" (Section 2)—exactly the skill that students learning formal mathematics need to develop. An instructor teaching a course on Lean/mathlib could use ProofNet's natural language statements as exercises: students read the informal theorem, attempt to formalize it in Lean, and compare their formalization against the ground-truth formal statement. The benchmark covers analysis, algebra, linear algebra, and topology, making it suitable for multiple courses. The case studies (Section 5.3) provide concrete examples of common errors (missing typeclass constraints, using nonexistent identifiers) that instructors can use as teaching material. The 13.4% Code-davinci-002 baseline establishes a "competency floor"—students can measure their progress against a known model performance level.

Automated data augmentation for formal mathematics libraries. The distilled backtranslation method, while achieving only 3.2% accuracy, provides a template for semi-automated expansion of formal libraries. A workflow: a mathematician writes a formal theorem in Lean; Code-davinci-002 (or a future, stronger teacher model) generates a synthetic natural language version; a human curator quickly verifies or edits the informalization (which is easier than writing it from scratch); the resulting (informal, formal) pair is added to a growing parallel corpus that can be used to train better autoformalization models. The paper's demonstration that purely synthetic data provides a training signal (3.2% for PROOFGPT-1.3B) suggests that even noisy synthetic pairs have value, and adding human curation would improve quality. This creates a positive feedback loop: more parallel data → better autoformalization models → easier formalization of new mathematics → larger formal libraries → more training data for even better models.

Quality assurance for neural theorem proving systems via autoformalization checking. Neural theorem provers that operate on formal statements (like those evaluated on miniF2F) assume the formal statement is correct. In a deployment setting where users provide natural language theorems and expect formal proofs, an autoformalization system first translates the informal statement to a formal statement, then a prover attempts to prove it. A failure mode is that the autoformalization produces a type-correct but semantically wrong formal statement, which the prover might then "prove" (since it's a different, potentially easier theorem). ProofNet's accuracy/typecheck ratio (≈0.5 for Code-davinci-002) quantifies this risk: even when the system produces valid Lean, it's wrong half the time. This suggests a practical safeguard: deploy informalization as a consistency check. After autoformalizing an informal statement to a formal statement, run informalization on the formal statement and check whether the round-tripped informal statement is semantically equivalent to the original. Code-davinci-002 achieves 62.3% informalization accuracy, providing a reasonably reliable verification signal, and the paper's recommendation to track all three metrics (accuracy, typecheck rate, BLEU) provides a monitoring framework for such a system.