Primary evidence
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal ProofsS1 · Primary research · Paper · 2022-10-21
- Draft, Sketch, and Prove implementation and result artifactsS1 · Primary research · Repository
Draft, Sketch, and Prove uses informal proofs to guide formal proof search
Language models produce a high-level formal sketch whose subgoals are then discharged by an automated prover.
What happened?
DSP mapped informal proofs into formal sketches and raised automated proving performance from 20.9% to 39.3% on a competition-problem collection.
Why it matters
The architecture anticipated later systems that alternate natural-language decomposition with verifier-backed formal proof.
Significance rationale: DSP made informal reasoning an explicit intermediate representation between language models and formal theorem provers.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Informal, Formal, Hybrid
- AI contribution
- Language models draft and sketch proof structure; formal provers verify and complete subproblems.
- Human contribution
- Researchers designed the three-stage workflow and constructed evaluation problems and prompting procedures.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-11
Technical details
- Systems
- draft-sketch-prove
- Organizations
- meta-ai, university-of-cambridge
- Problems
- competition-mathematics
- Methods
- autoformalization, proof-sketch, language-model
Sources & artifacts
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal ProofsS1 · Primary research · Paper · accessed 2026-09-10
- Draft, Sketch, and Prove implementation and result artifactsS1 · Primary research · Repository · accessed 2026-09-11
- Draft, Sketch, and Prove implementation and result filesArtifact · Code
Verification history
- 2022-10-21 · Paper released · E2 · Research record
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
This corpus refresh added a directly inspectable public artifact maintained by the authors or releasing organization. E3 records artifact-level inspectability and does not imply independent verification of the underlying scientific or mathematical claim.
Corrections
No corrections recorded.