Primary evidence
- Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem ProversS1 · Primary research · Paper · 2010-07-14
Sledgehammer makes external automated provers practical inside Isabelle
Sledgehammer selects relevant Isabelle facts, translates proof obligations to external ATPs and uses the returned information to help construct proof-assistant-checked proofs.
What happened?
At PAAR-2010 on 14 July 2010, Lawrence Paulson and Jasmin Blanchette presented three years of experience with Sledgehammer as a practical link between Isabelle and automatic theorem provers.
Why it matters
The system made strong automation accessible in routine interactive proving and became an important precedent for later AI assistants that orchestrate external search while retaining trusted proof checking.
Significance rationale: Sledgehammer established a practical architecture for combining an interactive proof assistant with powerful external ATP systems, automatically selecting relevant facts and turning external search into proof-assistant-native progress.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Substantive AI support
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Automated premise selection and external provers supplied substantial proof search, while Isabelle retained the trusted formal proof environment.
- Human contribution
- Researchers designed the translation, relevance filtering, prover orchestration and proof reconstruction mechanisms; users supplied formal goals and integrated resulting proof steps.
- Verification
- Paper released · E2 · Research record · Machine-checked
- Last reviewed
- 2026-09-15
Technical details
- Systems
- sledgehammer, isabelle
- Organizations
- university-of-cambridge
- Problems
- interactive-theorem-proving
- Methods
- premise-selection, automated-theorem-proving, proof-reconstruction
Sources & artifacts
- Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem ProversS1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 2010-07-14 · Paper released · E2 · Research record
The PAAR-2010 program and proceedings document Sledgehammer's practical Isabelle/ATP workflow; machine checking refers to proof-assistant validation of reconstructed formal proofs, not independent reproduction of reported usage results.
Corrections
No corrections recorded.