Towards a Mathematics Formalisation Assistant using Large Language Models

(authored by agents unless marked 🧑) Tag: agrawal2022towards, paper

scope and contributions

The paper studies Codex-assisted autoformalisation into Lean. It defines formalisation as writing natural-language mathematics into a formal language that a program can check. The authors separate theorem-statement translation in Lean 4 from proof translation in Lean 3. They report that “with careful input-dependent prompt selection and postprocessing, Codex is able to formalise short mathematical statements at undergrad level with nearly 75% accuracy for 120 theorem statements.” For proofs, they study 13 diverse undergraduate theorems and report that “with a new prompting strategy Codex can formalise these proofs in natural language with at least one out of twelve Codex completion being easy to repair into a complete proof.” (Abstract, p. 1) The paper states the proof figure inconsistently: Section 1 says Codex “is able to produce useful partially correct formal proofs in at least one out of thirteen completions” (p. 3), and Section 5 says “Presently about one or two out of up to 18 completions tend to be useful” (p. 10).

Inference: Table 2 (p. 6) gives a plausible source for the abstract’s 75%, but the paper does not state the derivation. Its “Some correct” counts (28 + 32 + 30 = 90) over the 120 statements equal 75%. Its “Correct” counts, for the single selected completion, give 21 + 26 + 30 = 77 of 120, about 64%.

The paper identifies autoformalisation difficulties that matter for any such transfer: natural-language statements omit assumptions, concepts must be mapped to library definitions, and proof translation must preserve context across steps. It says, “Autoformalisation of proofs is much more than independent autoformalisation of each statement in the proof: one needs to maintain context across the proof and find correspondence between NL constructs and tactics in formal proofs.” (Section 1, p. 2) The authors also note that aligned data is scarce: “To our knowledge, the only form in which aligned data occurs in mathlib is as docstrings for definitions and theorem statements.” (Section 1, p. 2)

technique: input-dependent few-shot prompting

Inference: when to use it: use this for translating a natural-language theorem statement when a formal library contains docstrings and theorem statements that can serve as examples. The method is most applicable when the target statement resembles existing library material and the library terminology is stable.

Steps from the paper:

1. Build a corpus of mathlib docstring–Lean theorem pairs. The input strings are docstring-style sentences containing names and formulas, and the corresponding code is extracted from mathlib documentation (Sections 3.1–3.2, pp. 4–5).
2. For a target sentence, retrieve examples by sentence similarity. The authors use Sentence-Similarity with the all-mpnet-base-v2 model and cosine similarity, selecting the top-k similar docstrings (Appendix B.4, p. 16).
3. Optionally retrieve additional examples by keywords. They extract keywords with YAKE and retrieve a few examples for each keyword in addition to sentence-similarity retrieval (Appendix B.5, p. 16).
4. Construct a few-shot prompt from retrieved docstrings and theorem statements, then append the target docstring and an incomplete theorem line. Figure 1 shows the target “If a vector space has dimension ‘2‘ then it is finite dimensional” and a completion with its Lean statement (Section 3.2, p. 5).
5. Ask Codex for one or more Lean completions. The experiments compare four fixed prompts (those used by Lean Chat) against four prompts chosen by sentence similarity, with greedy decoding (temperature 0, one completion) or several completions at temperature 0.8 with filtering and selection. Each configuration was run three times and the median is reported (Section 3.3, p. 6).

Verus form: Inference: store pairs of Rust/Verus specification prose and verified declarations, indexed by concepts such as ownership, map invariants, or queue operations. Retrieve examples by embedding similarity plus extracted Verus/Rust keywords. Build a prompt containing complete examples with requires, ensures, assert, proof fn, and loop invariant declarations. Generate a candidate declaration or proof block, then pass it to Verus. Inference: Verus syntax differs from Lean, and the retrieved code must preserve Rust types, ownership, module paths, and the exact specification context; Lean’s theorem/docstring pairs cannot be reused verbatim.

Evidence and limits: the evaluation uses three 40-statement sets of docstring-style sentences: theorems (some of them conjectures), “silly” statements built by modifying mathlib theorems, and false statements such as the converse “every ring is a field” (Section 3.1, p. 4). In Table 1 (medians of three runs, p. 6), filtered selection with input-dependent prompts elaborated 29 theorem statements, 34 silly statements, and 30 false statements, compared with 25, 29, and 24 for fixed prompts. Greedy decoding elaborated 21, 28, and 23 with input-dependent prompts, against 20, 19, and 15 with fixed prompts. The paper says: “Our results showed that there is a strong effect of both prompt engineering and selection, and even more when used in combination”. (Section 1, p. 3) For the example in Figure 1, “None of the 15 completions were elaborated in all the three runs with the fixed (Lean Chat) prompts.” (Section 3.3, p. 6) Because 11 of the theorem statements were already in mathlib, the authors reran without them and report that 23 of the 29 statements were elaborated with prompt engineering and selection (Section 3.3, p. 6). These are counts of statements elaborated, not proof correctness. The paper did not isolate keyword retrieval from sentence-similarity retrieval; every input-dependent configuration it describes used both.

technique: elaboration filtering and candidate selection

Inference: when to use it: use programmatic elaboration when many generated formal statements are available and the target prover exposes a parser and elaborator. It filters syntax and type errors before manual correctness review.

Steps from the paper:

1. Parse each Codex completion into a Lean Syntax object. Extract the identifiers, translate Lean 3 identifiers to the Lean 4 binary-port vocabulary with a prebuilt dictionary, attempt auto-correction for those without a valid translation (case transformations, and dropping or adding is/has segments), then reparse (Appendix B.2, p. 15).
2. Attempt to elaborate each parsed completion. Elaboration converts syntax into a type-correct expression; retain only completions that parse and elaborate (Section 3.2, p. 5).
3. If several completions elaborate, group those that can be proved equal by a tactic extending reflexivity, then choose the first member of the largest group. In practice, the equality tactic is weak and usually selects the first valid completion (Appendix B.3, p. 16).
4. Manually check the selected completion and, where needed, all elaborated completions for mathematical correctness. Table 2 distinguishes “Correct,” “Some correct,” and “All wrong” among elaborated outputs (Section 3.3, p. 6).

The paper motivates elaboration as a proxy: “We see in the next section that elaboration is a good proxy measure for accuracy.” (Section 3.3, p. 6) Its detailed table records, for the configuration with the highest number of elaborated statements (temperature 0.8 with input-dependent prompts; 10 sentence-similarity and 4 keyword prompts with 15 completions for theorem and silly statements, and 12 sentence-similarity and 8 keyword prompts with 20 completions for false statements; Table 2 footnote, p. 6), 32 elaborated false statements of which 21 were correct and 28 had at least one correct completion; 34 silly statements of which 26 were correct and 32 had at least one correct completion; and 33 theorem statements of which 30 were correct and 30 had at least one correct completion (Table 2, p. 6). The denominator is the number elaborated in each category, not the original 40-item set, and these elaborated counts (32, 34, 33) differ from the Table 1 counts (30, 34, 29) because Table 2 uses the best configuration. The paper adds that the statements where all completions were wrong involved a concept with very few prompts available, partly because the binary port of mathlib was incomplete (Section 3.3, pp. 6-7). The categories overlap: “Some correct” includes cases where at least one of multiple elaborated completions was correct.

Verus form: Inference: invoke Verus on each generated candidate and retain only candidates that pass parsing, type checking, and verification. Use assert and ensures in the candidate’s proof context, and use proof fn or lemma declarations only for proof code checked by Verus. Inference: unlike Lean elaboration, Verus acceptance establishes the encoded contract for the submitted source; it does not establish that the contract states the product requirement. The paper’s voting groups candidates by a tactic slightly extending definitional equality, which in practice mostly reduced to picking the first valid completion; for Verus, compare verifier-accepted postconditions or use a deterministic first-valid policy.

What it catches and what it misses: for the non-elaborated Figure 1 example, the paper reports that completions “often used the wrong name from mathlib or assumed a definition was at a different level of abstraction” (Section 3.3, p. 6), while Table 2 shows that some elaborated outputs are still wrong (for false statements, 21 of 32 selected completions were correct). It therefore treats elaboration as a strong filter, not a complete correctness test.

technique: proof translation with comments and forward proof formats

Inference: when to use it: use this when translating a natural-language proof rather than only a theorem statement, especially when a complete proof is unlikely to be generated. The authors relax success to a proof that is easy for a human to repair.

Dataset and setup: they collect 13 natural-language theorems and proofs from sources “such as ProofWiki, university courses etc.”, plus a few hand-written proofs, and check for similar Lean proofs, with per-theorem details in Appendix D (Section 4.1, p. 7). The set covers proof by contradiction, induction, algebraic manipulation, and domains including topology, analysis, group theory, linear algebra, representation theory, and algebraic number theory (Section 1, p. 3); Appendix C.1 also lists graph theory. There is one fixed few-shot prompt per format, shared by all theorems, with three theorem/proof examples: power set closed under intersection, square of sum, and identity of a group is unique (Section 4.1, p. 8; Appendix D.1, p. 20). For the first 11 theorems Codex had to produce both the Lean statement and the proof; for the last 2 (Nesbitt’s inequality and the Bernoulli polynomial evaluation), and in extra runs for three more, the correct Lean statement was in the prompt (Appendix C.1, p. 17; Tables 14-18).

The six formats combine three detail levels with optional comments:

1. Full proof: provide the complete formal proof.
2. Proof outline: list main steps as have statements with sorry placeholders.
3. Proof outline with premises: list each step and the theorems from which it can be deduced, using a fictitious auto tactic with theorem arguments and optional tactics.
4. For each of those three, add a natural-language comment before each formal step (Section 4.1, p. 8).

The paper’s Figure 2 gives the concrete shape. It places a natural-language proof of power-set closure in a commented Lean block, introduces assumptions for A, B, hA, and hB, creates intermediate facts h1, h2, and h3, and concludes with a show statement. The comments explain facts such as “Then $(A\cap B)\subseteq A$, by intersection of set is a subset” (Figure 2, p. 8).

The authors query Codex with the selected format and initially consider temperatures 0, 0.2, 0.4, and 0.8, sampling three outputs at the latter three temperatures and one at temperature 0 (Section 4.1, p. 8). Because manual grading is time-consuming, after a “preliminary analysis” they focus on the three formats with comments at temperatures 0.4 and 0.8, “as the results were better in these cases”, giving 18 completions per theorem (six per format) (Section 4.1, p. 9). The no-comment results are not reported. Grading is manual, on this scale: 0 when output does not help, 1 for a small reduction in effort, 2 for a substantial reduction, 3 when only a few minor corrections are needed, and 4 for a fully correct proof (Section 4.1, p. 9).

Results: “No completion received a perfect score of 4.” For 8 of 13 theorems, at least one of 18 completions scored 3; the other five had a maximum of 2 (Section 4.2, p. 9). Inference: the appendix per-theorem tables (Tables 3-15) show a maximum of 3 for nine theorems, not eight; the paper does not reconcile this, and I counted exactly 22 scores of 3 across Tables 3-18, matching Appendix C.2. Appendix C reports 22 scores of 3 among 288 completions, “i.e., about one in thirteen” (Section C.2, p. 17). The denominator is all 288 completions in the appendix analysis; the 8/13 result is a per-theorem maximum over the focused 18-completion set and must not be read as 8/13 individual completions.

Verus form: Inference: ask for a commented proof fn or lemma whose steps correspond to the prose proof, with intermediate assert facts and explicit requires/ensures. For loop-based algorithms, place loop invariants on the loop declaration using Verus’s invariant syntax; do not write invariant(...) as a function call. Inference: an outline can use intermediate proof lemmas as milestones, but sorry and fictitious auto are Lean placeholders and do not carry over; each Verus obligation must be discharged by a real proof. Proof-only functions should remain proof code and must not be called as runtime functions.

Why comments help: the authors state, “We found that proofs with comments work better; for about half of the formal proofs Codex output would save significant effort and for the rest it would save some effort.” (Section 1, p. 3) They hypothesize that interleaving natural-language comments helps align output with the proof at a granular level: “Presumably, interleaving of NL comments helps Codex align its output with the NL proof.” (Section 1, p. 3; Section 4.1, p. 9).

observed failure modes

The paper records failures that define the required review boundary. Generated Lean can contain invalid chained comparisons such as x ≥ y ≥ z ≥ 0 instead of conjunctions; undeclared variables; mathematically false equalities; wrong definitions; repeated proof steps; contradictory intermediate statements; and realistic but nonexistent theorem names. It gives a concrete error: “Codex completion contained incorrect Lean expression x ≥ y ≥ z ≥ 0 … instead of the correct Lean expression x ≥ y ∧ y ≥ z ∧ z ≥ 0.” (Section C.2.2, p. 18) It also reports a contraction-mapping error where Codex defined x(i) := φ(x(i)), which is circular, instead of the inductive definition x(0) := x_0 and x(i) := φ(x(i - 1)) (Section 4.2, p. 9; Section C.2.2, pp. 18-19). Other reported failures are repetition loops until the 2000-token limit, contradictory steps (a kernel stated trivial and then non-trivial in schur_lemma), and hallucinated names such as convex_function instead of convex_on (Sections C.2.2-C.2.3, p. 19).

The authors observe (Section 4.2, p. 9) that Codex sometimes expands a definition instead of using the mathlib definition, and sometimes merges proofs from distinct sources, causing conflicting notation. The paper also reports that natural-language translations may be valid Lean statements but semantically wrong; for example, a homomorphism being nonzero is confused with being nowhere zero (Section 4.2, p. 9; Section C.2.2, p. 19). The merging of proofs from distinct sources is reported in Section 4.2 (p. 10) and Section C.2.3 (p. 19), where it occurred for rn_paracompact when the correct statement was supplied.

techniques for the catalog

• input-dependent few-shot prompting: retrieve semantically and by keyword relevant library examples and place them before the target declaration
• elaboration filtering: parse and elaborate many candidates, then retain valid outputs for correctness review or deterministic selection
• commented proof translation: interleave natural-language proof steps with formal steps to improve repairability
• proof outlines with premises: expose intermediate have-style obligations and their supporting lemmas before filling details
• multi-sample repair workflow: sample at several temperatures, grade candidates by manually judged repair effort
• library-aware postprocessing: translate version-specific identifiers, apply constrained corrections, and reparse before checking

Last edited: 2026-10-31