⊕ Датасет · mathlib-emb · v2.0
MathLib Embeddings
Векторные представления утверждений Mathlib моделями SciLibMath v2 / SciLibModal. 1 миллион векторизованных утверждений 312-dim, готовый Qdrant payload + dense vectors.
Готовый к загрузке датасет векторов: для каждого из 213 000 утверждений Mathlib получено по 5 эмбеддингов (формулировка EN, формулировка RU, Lean-сигнатура, Lean-тело, LaTeX) — итого порядка 1 миллиона 312-мерных векторов. Косинусная метрика, формат — Qdrant payload (JSON) + dense vectors.
Используется в проде SciLib для семантического поиска и для опциональной векторной аугментации Graph RAG (шаг 8 pipeline C21).
Доступ — через MCP-tool semantic_search или прямой запрос к Qdrant (для лабораторных групп — по запросу).
Теги: embeddings, vector, qdrant, mathlib, dense