---
issue: 1
status: working
tags: data
---
# premise-retrieval

Retrieve Mathlib premises by embedding before each tactic step.

## What happened

- Started.

## Next

Keep the lemmas proved along the way.