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

Retrieve Mathlib premises by embedding before each tactic step.

## What happened

- 2026-09-08: 71 problems proved (+7 on the baseline)
- 2026-09-15: 79 problems proved (+15 on the baseline)

## Next

Keep the lemmas proved along the way.