The exact ChromaDB index and serving code used as the leansearch tool in the
COLM 2026 paper "Awakening: minimal agentic replay recovers tool use in
formal-math fine-tuned LLMs." Every <tool_call> in the ProofNet runs of
awakening-proofnet-runs
was answered by this index.
160,998 Mathlib declarations, each with its Lean signature/type plus an
LLM-generated informal name and description (the Herald-style bilingual
representation… See the full description on the dataset page:
https://huggingface.co/datasets/juihuichung/awakening-leansearch-v4.9.0.
