Axiomatic Octo

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 axiomatic-octo

That installs what you need to search and to download prebuilt databases (~12 MB). Building your own index additionally needs the informalization LLM stack, which is an opt-in extra because it is 25× the size:

uv tool install 'axiomatic-octo[build-search-index]'   # adds `octo search index`

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 over the same OPENROUTER_API_KEY the embedder uses; without it, queries fall back to vector-ranked results.

cd my-lean-project
octo search fetch                                  # download prebuilt search databases
octo search status                                 # what's installed, and any updates
octo search 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 (octo search index, which needs the build-search-index extra above).

Layout

Names

The PyPI distribution and the marketplace extension are both axiomatic-octo, the module is axiomatic_octo, the commands are octo and octo-sidecar, and the extension settings are octo.*.

CLI verbs sit under a domain, so it is octo search query "..." rather than octo query "...". The domain level is there so later domains can be added under the one binary without disturbing these verbs.

These are stable surface now — renaming them again would break imports, configs, and keybindings. Everything was last renamed from ax-search-lean / axSearchLean.*; the extension migrates settings, the stored API key, and the search-database cache on first activation.

Development

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

uv run pytest                          # Python tests
uv run ruff check .                    # lint
pnpm --filter axiomatic-octo run test  # extension tests

uv sync includes the build-search-index extra (the dev group self-references it), so the whole test suite runs. To reproduce what an extension user gets — the wheel with no extras — build and install it into a scratch venv; the bare-install CI job does exactly this and asserts the query path still imports, since the dev environment can never catch a stray module-scope import of the index stack.

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/axiomatic_octo/protocol.py:

pnpm --filter axiomatic-octo run protocol:codegen

CI asserts the generated file is up to date.

License

AGPL-3.0-only. See LICENSE.