Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

1 INTRODUCTION

• Formal proof automation faces a shortage of formal data because proof formalization is difficult and accessible to few experts, whereas informal mathematical proofs are abundant.Source: §1 · p. 2
• DSP uses formal proof sketches of high-level reasoning steps from informal proofs to guide an automated prover toward a full formal proof.The sketches contain intermediate conjectures without justification, which the automated prover attempts to prove.Source: §1 · p. 2
• The authors build a dataset of manually curated informal statements and proofs aligned with formal statements in miniF2F.Source: §1 · p. 2
• On miniF2F, language-model-generated informal proofs increase the automated prover’s solved-problem proportion from 20.9% to 38.9%; with human-written proofs, it reaches up to 39.3%.Source: §1 · p. 2
• Three ablations examine the benefits of drafting informal proofs, annotating sketches with informal segments, and using automated provers to close open conjectures.Source: §1 · p. 2

Interactive theorem proving

• Interactive theorem provers such as Isabelle, Lean, Coq, and Metamath use logical kernels to check theorems, while formal proofs reduce stated theorems to proven facts through simpler subgoals.The paper distinguishes kernel-verified formal proofs from informal proofs written in standard mathematical language.Source: §2 · pp. 2–3

Machine learning for formal proof synthesis

• Prior formal-proof synthesis typically uses sequence-to-sequence models under 1 billion parameters to propose proof steps and search subgoals with methods such as MCTS; this paper uses fewer model calls and models up to 175 billion parameters.The cited approaches condition on the current proof state; the paper’s larger models are motivated by few-shot learning.Source: §2 · p. 3

Machine learning for informal reasoning

• Informal mathematics models can produce false positives—correct answers with incorrect proofs—and these errors become more frequent on harder problems, whereas ITP-checked formal proofs are guaranteed correct.The paper builds on this concern by translating informal proofs into formal proofs.Source: §2 · p. 3

Autoformalization

• After prior work on statement autoformalization, including few-shot translation by large language models (Wu et al., 2022), this paper investigates whether such models can autoformalize proofs.Earlier work included a position paper, synthetic-data experiments evaluated by text similarity (Wang et al., 2020), and few-shot statement translation.Source: §2 · p. 3

3 METHOD

• DSP formalizes problems with informal and formal statements by using informal proofs to guide automated theorem provers through a three-stage pipeline.The stages are drafting, sketching, and proving.Source: §3 · p. 3

3.1 DRAFTING INFORMAL PROOFS

• The drafting stage uses available human-written proofs or asks a language model to generate candidate proofs when ground-truth proofs are absent.The model can produce multiple alternatives, and a draft need only help generate a good formal sketch in the next stage; its correctness need not be automatically verified.Source: §3.1 · p. 3

3.2 MAPPING INFORMAL PROOFS INTO FORMAL SKETCHES

• A few-shot autoformalizer maps informal proofs into formal sketches that preserve high-level structure while leaving low-level details for an automated prover.The model is prompted with example informal-proof/formal-sketch pairs because large parallel corpora are unavailable. In the Figure 2 example, the sketch uses five intermediary conjectures and marks open conjectures for later proving.Source: §3.2 · p. 4, Figure 2 · p. 4

3.3 PROVING OPEN CONJECTURES IN THE SKETCHES

• Off-the-shelf automated provers fill sketch gaps, and the evaluation counts success only when all gaps are closed and the resulting proof checks against the specification.The framework permits symbolic, neural-network-based, or hybrid provers; exceeding the time limit counts as failure.Source: §3.3 · p. 4

4.1 DATASET AND EVALUATION

• The evaluation uses Isabelle on 488 miniF2F problems, split into 244-problem validation and test sets.A proof counts only if it avoids sorry and oops and Isabelle verifies it; Isabelle was selected for its proof corpus, declarative proof style, and Sledgehammer automation.Source: §4.1 · p. 5

4.4 RESULTS

• 39.3% test success with human-written proofs exceeds the 20.9% test success of Sledgehammer + heuristics.DSP with human proofs also achieves 42.6% validation success and proves 200 of 488 problems.Source: Table 1 · p. 6, §4.4 · pp. 6–7
• Minerva 62B reaches 43.9% validation and 37.7% test success, while Minerva 540B reaches 42.6% validation and 38.9% test success.Codex and Minerva 8B each reach 40.6% validation and 35.3% test success; Minerva 62B solves 199 problems, one fewer than human proofs, and Minerva 540B also solves 199.Source: Table 1 · p. 6, §4.4 · p. 7

4.3 EXPERIMENTAL SETUP

• For model-generated proofs, DSP samples 100 informal proofs per problem, prompts Codex with three examples and the current problem, then proves each open sketch conjecture.The 20 manually prepared examples are evenly divided between algebra and number theory; the prover used is Sledgehammer + heuristics.Source: §4.3 · p. 6

4.2 BASELINES

• On miniF2F, the 11-tactic baseline raises Sledgehammer success from 9.9% to 18.0% on validation and from 10.4% to 20.9% on test.Thor and Thor + expert iteration achieve 29.9% and 35.2% test success, respectively; Lean-based methods are not directly comparable because they use a different prover.Source: §4.2 · p. 5, §4.4 · p. 6, Table 1 · p. 6

5.1 ABLATION STUDIES

• Without inline comments, miniF2F success fell 4.9%/2.8% on validation/test; without informal drafts, it fell 3.7%/5.3% versus human proofs; without automated provers, it fell 9.8%/9.0%.The reported validation/test drops show that comments, informal drafts, and automated provers each contribute to DSP’s success.Source: §5.1 · p. 7
• With human proofs, DSP reached a plateau after 70 attempts, while removing comments plateaued around 50 and removing informal proofs around 70; removing sketches solved 154 problems.The no-comment and no-informal-proof variants solved 181 and 178 problems, respectively, whereas human-proof DSP needed only 7 attempts to reach the no-sketch variant’s performance.Source: §5.1 · pp. 7–8, Figure 3 · p. 8

5.2 LANGUAGE-MODEL-GENERATED PROOFS

• Minerva-generated informal proof drafts enabled a successful formal proof of IMO problem imo 1959 1, unlike the human proof.The authors hypothesize that some human proofs leave gaps too difficult for automated provers, while diverse language-model proofs may be more amenable to them.Source: §5.2 · p. 8, Figure 4 · p. 9
• Of 50 Minerva proofs that formalized successfully, 29 (58%) were entirely correct, 16 had an identifiable incorrect step, and 5 were nonsensical.The 21 incorrect or nonsensical proofs still led to successful formal proofs: the prover largely ignored 13, while the autoformalizer corrected errors in 8, suggesting robustness to flawed inputs.Source: §5.2 · p. 8
• After filtering problems solvable directly by the automated prover, 21 of 27 Minerva proofs were correct and 6 had small errors; the filter achieved 77.8% precision and 72.4% recall.None of the 27 remaining proofs were nonsensical.Source: §5.2 · p. 9
• 209 theorems (111/98 on valid/test) were solved with Minerva-generated drafts after 200 attempts, versus 203 (106/97) with human drafts, suggesting draft diversity can help.The 62B and 540B Minerva models had comparable performance and consistently outperformed the 8B Minerva and Codex models; human drafts solved more problems for 1–100 attempts, but the difference was one problem at 100 attempts.Source: §5.2 · pp. 9–10, Figure 5 · p. 10
• With a fixed budget of fewer than 100 sketches per problem, allocating more attempts to distinct Minerva (540B) drafts yielded the most miniF2F successes.The experiment varied the number of informal drafts and sketches per draft under the same total-sketch constraint.Source: §5.2 · p. 10, Figure 5 · p. 10

5.3 MEMORIZATION

• The authors argue that it is inappropriate to attribute the models’ abilities to memorization: they report no evidence that Minerva’s abilities come from memorization, and Codex training data predated miniF2F’s public release.The cited Codex training cutoff is before June 2021.Source: §5.3 · p. 10

• DSP reached state-of-the-art performance on miniF2F with Isabelle, and ablations show automatic conversion of informal proofs to sketches is critical.The sketches mirror informal proofs’ high-level reasoning structures.Source: §6 · p. 11
• DSP constructs the formal proof structure from an informal proof in one decoding operation, leaving the prover to fill gaps between intermediate conjectures.Unlike approaches using only formal data, DSP benefits by design from informal proofs.Source: §6 · p. 11
• DSP currently uses a purely symbolic prover; future work targets stronger search such as HyperTree Proof Search (Lample et al., 2022) and more efficient sketch generation.The authors found generation count crucial for performance, as in AlphaCode (Li et al., 2022), and identify autoformalizer computational cost as a bottleneck.Source: §6 · p. 11

CODE AND DETAILED RESULTS

• Experiment-reproduction code and additional main-experiment result details are available at github.com/albertqjiang/draft sketch prove.Source: CODE AND DETAILED RESULTS · p. 11

• AQJ and WL are supported by ERC Advanced Grant ALEXANDRIA (Project GA 742178), and AQJ also receives a Peterhouse Graduate Studentship.Source: FUNDING DISCLOSURE · p. 11

LIST OF CONTRIBUTIONS

• AQJ conceived using proof sketches and conducted the experiments.Source: LIST OF CONTRIBUTIONS · p. 11
• SW constructed the first pipeline version and initial autoformalization prompts.Source: LIST OF CONTRIBUTIONS · p. 11
• JPZ produced Minerva informal proofs and helped conduct autoformalization experiments.Source: LIST OF CONTRIBUTIONS · p. 11
• GL proposed inline comments in formal proof sketches to improve alignment.Source: LIST OF CONTRIBUTIONS · p. 11
• JPZ, YW, and SW conducted case analyses of Minerva solutions.Source: LIST OF CONTRIBUTIONS · p. 11
• AQJ, TL, GL, SW, and JL contributed to the dataset; AQJ and WL wrote the final autoformalization prompts.Source: LIST OF CONTRIBUTIONS · p. 11
• AQJ, GL, SW, and TL wrote the paper, while YW and GL directed the project.Source: LIST OF CONTRIBUTIONS · p. 11

A CONJECTURES AND THE DECLARATIVE PROOF STYLE

• Interactive theorem provers such as Isabelle and Mizar use declarative proofs interleaving conjectures with their corresponding proofs.Source: A CONJECTURES AND THE DECLARATIVE… · p. 15
• Syme (1997) argued that a declarative proof’s conjectures should resemble a mathematical-textbook proof sketch and sufficiently convince the reader.Source: A CONJECTURES AND THE DECLARATIVE… · p. 15
• In practice, interactive theorem-prover users write a list of conjectures as a formal sketch, then use automation to fill each gap.Source: A CONJECTURES AND THE DECLARATIVE… · p. 15

B SLEDGEHAMMER

• Sledgehammer automates Isabelle reasoning by flattening Isabelle/HOL goals into other logics for automated theorem provers.The listed provers include E, CVC4, Z3, Vampire, and SPASS.Source: B SLEDGEHAMMER · p. 15
• When an automated prover succeeds, Sledgehammer reconstructs its proof in Isabelle/HOL using certified provers, yielding a relatively more human-interpretable proof.The certified provers named are metis, meson, and smt.Source: B SLEDGEHAMMER · p. 15
• For the conjecture that 4 divides a natural number only if 2 does, Sledgehammer may return a meson proof using transitivity of divisibility and the evenness of 4; otherwise it reports failure or timeout.Source: B SLEDGEHAMMER · p. 15

A Proof to an International Mathematical Olympiad Problem

• DSP formalized Minerva’s solution to IMO 1959 P1, the first problem of the first International Mathematical Olympiad.The informal problem, Minerva-generated solution, and DSP formal proof are shown together in Figure 4.Source: C A PROOF TO AN INTERNATIONAL… · p. 15
• DSP copied parts of Minerva’s informal proof into comments before corresponding formal blocks and selected premises after stating conjectures, including some unnecessary ones.It omitted the informal solution’s first sentence because that sentence was identical to the formal statement.Source: C A PROOF TO AN INTERNATIONAL… · p. 15
• The formal proof’s five conjectures were proved by the automated prover, but one gcd step required SMT and Z3 plus 10 external lemmas or facts.The paper says it is highly unlikely that either the language model or automated theorem prover could finish this proof alone.Source: C A PROOF TO AN INTERNATIONAL… · p. 15
• The human proof’s indirect gcd notation produced a semantically incorrect conjecture that the automated prover could not close, unlike Minerva’s explicit Euclidean-algorithm steps.The human-written proof did not yield a successful formal proof; its sketch’s ATP step was marked unsuccessful.Source: C A PROOF TO AN INTERNATIONAL… · pp. 15–16

Human algebra example

• A human algebra proof guided the sketch to split the problem into three cases and derive a contradiction in each before proving the objective.The figure describes the resulting formal sketch as complex and consistent.Source: Figure 6 · p. 17

Minerva algebra example

• A Minerva algebra proof yielded a sketch with five intermediate conjectures, excluding ATP-tagged lines and aligning inline comments with the informal proof.Source: Figure 7 · p. 18

Alternative proofs

• Alternative Minerva and human proofs produced sketches that followed their distinct strategies, made cases explicit, and selectively omitted or synthesized steps.The Minerva sketch made even and odd cases explicit, with three conjectures per case, and excluded an unnecessary divisibility claim. The human sketch used residues modulo 4, synthesized an intermediate step, and omitted the informal proof’s last step.Source: Figure 8 · p. 19

Three types of Minerva proofs

• Codex formalized a slightly incorrect Minerva proof by changing its base case from n = 1 to case 0, but also directly proved a statement from a meaningless one-line proof.The correction reflects that natural numbers include 0; the direct proof suggests Codex considered the problem simple.Source: Figure 9 · p. 20