# Proof-Pattern Recognition and Lemma Discovery in ACL2

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Aug 2013.

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

- [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)
- [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (2025)
- [Conjectures, Tests and Proofs: An Overview of Theory Exploration](https://mlsanity.com/paper/2109.03721/) (2021)

## Abstract (arXiv)

We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition to pre-processes data from libraries, and then suggests auxiliary lemmas in new proofs by analogy with already seen examples. This paper presents the implementation of ACL2(ml) alongside theoretical descriptions of the proof-pattern recognition and lemma discovery methods involved in it.