Axiomatic Lean Search

Semantic search over Lean 4 declarations — Mathlib, core, Batteries, and your own Lean projects. Ask in plain English and get matching declarations, ranked by meaning rather than name. Ships a Python CLI and JSON-RPC sidecar plus a VS Code extension.

Install

VS Code (recommended): install the extension from the Marketplace and open a Lean project. On first activation it sets up everything it needs — including its own Python — with no manual steps.

CLI only:

uv tool install ax-assistant-release-staging

Quickstart

Queries embed your text with qwen3-embedding-8b via OpenRouter, so an API key is required. Export OPENROUTER_API_KEY, or put it in a .env.secrets file in your project root (the current directory, the --folder target, and a user-global config file are checked in that order; shell environment always wins). Results are reranked with Qwen3-Reranker-8B when SILICONFLOW_API_KEY is also set; without it, queries fall back to vector-ranked results.

cd my-lean-project
ax-search-lean fetch                                  # download prebuilt search databases
ax-search-lean status                                 # what's installed, and any updates
ax-search-lean query "self-adjoint operator is symmetric"

Search databases are SQLite files with sqlite-vec vector indexes, either downloaded prebuilt or built locally from a Lean project (ax-search-lean index).

Layout

Names

The PyPI distribution is ax-assistant-release-staging (provisional; see TODO-packaging.md), the module is ax_assistant_public, the commands are ax-search-lean and ax-search-lean-sidecar, and the extension settings are axSearchLean.*. The module, command, and setting names are stable surface — renaming them would break imports, configs, and keybindings.

Development

uv sync                                # Python deps + editable install
pnpm install                           # extension deps

uv run pytest                          # Python tests
uv run ruff check .                    # lint
pnpm --filter ax-assistant-release-staging run test  # extension tests

To run the extension from source, open this repo in VS Code and launch "Run Search Extension (isolated)" (F5). It loads only this extension and resolves the sidecar from the repo .venv, so an installed release can't shadow your working copy.

Regenerate the TypeScript protocol bindings after changing src/ax_assistant_public/protocol.py:

pnpm --filter ax-assistant-release-staging run protocol:codegen

CI asserts the generated file is up to date.

License

AGPL-3.0-only. See LICENSE.