What this is: A small, reproducible demo adapter for Qwen/Qwen3-Embedding-0.6B that enables lightweight, LLM-free semantic search over mathlib (Lean 4). Supports both natural language and formula-based search (can be used in combination) for finding Lean theorems or mathematical statements. Does not support LaTeX syntax search yet.

Data is built from ~180k Lean theorems extracted via LeanDojo for Lean 4.20.1 (there may be minor gaps vs. the full mathlib).

Part of the AITP 2025 submission: “Towards Lightweight and LLM-Free Semantic Search for mathlib4.”

adapter/adapter_config.json & adapter/adapter_model.safetensors — LoRA weights for the encoder
faiss/<*.idx> — HNSW FAISS index (built for cosine/inner-product search)
faiss/*public_index.jsonl — public mapping { idx, full_name, statement }

DEMO

https://github.com/IsaacLi74/Lightweight-and-LLM-Free-Semantic-Search-for-mathlib4

Isaac74/qwen3-0.6b-lightweight-semantic-mathlib-search-adapter

Lightweight Semantic Mathlib Search — LoRA Adapter (Demo)

Contents

DEMO

Isaac74/
qwen3-0.6b-lightweight-semantic-mathlib-search-adapter