Draft, Sketch, and Prove
DSP
Maps informal mathematical proofs into formal Isabelle/HOL proof sketches and discharges the open subgoals with Sledgehammer ATPs.
The loop
- Proposes
An LLM drafts an informal mathematical proof and translates it into a formal Isabelle/HOL proof sketch with open `sledgehammer` subgoals.
- Judged by
Isabelle/HOL and automated theorem provers (E, SPASS, Vampire, Z3, CVC4 via Sledgehammer) verify each intermediate step.
- Steers
Sketches are sampled independently; a problem counts as solved if any sketch is completed.
Headline result
Solved 39.3% of miniF2F test theorems in Isabelle/HOL, a more than 10 percentage point jump over prior direct tactic-generation baselines.
What this does not prove
If the high-level proof sketch omits a bridge lemma too large for Sledgehammer to close within its timeout, the whole sketch fails.
How it generalizes the harness
- The algorithm is the solver
- A domain authority judges
- The output outlives the model
- An infallible formal kernel
The LLM supplies the high-level proof skeleton while superposition and SMT theorem provers (Sledgehammer) discharge the leaf obligations.
Classification
| What it proposes | Proof |
|---|---|
| Generative model | Minerva / Codex formal sketch generator |
| Algorithmic authority | Isabelle/HOL kernel and Sledgehammer automated theorem provers |
| Feedback | Proof state |
| What gets updated | Population of candidates |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Code released |
| Lineage | Original system |