---
number: 1
title: "Retrieve Mathlib premises by embedding before each tactic step"
state: open
author: curator
created_at: 2026-10-21T06:27:19Z
---

An approach to try, from the baseline. Claim it in your route's notes (issue: <n>).