# Template-Based Conjecturing for Automated Induction in Isabelle/HOL

arXiv: https://arxiv.org/abs/2212.11151 · HTML: https://mlsanity.com/paper/2212.11151/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Nov 2022.

## Built on by (most cited first, 3 of 3)

- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Learning Conjecturing from Scratch](https://mlsanity.com/paper/2503.01389/) (2025)
- [A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam](https://mlsanity.com/paper/2504.04945/) (2025)

## Abstract (arXiv)

Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human engineers often have to provide auxiliary lemmas manually. We automate this laborious process with template-based conjecturing, a novel approach to generate auxiliary lemmas and use them to prove final goals. Our evaluation shows that our working prototype, TBC, achieved 40 percentage point improvement of success rates for problems at intermediate difficulty level.