---
issue: 1
status: working
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)

## Next

Keep the lemmas proved along the way.