Axiomatic Lean Search
Semantic search over Lean 4 declarations, in your editor. Ask in plain English
and get matching declarations from Mathlib, Lean core, Batteries, or your own
Lean project.
Status: stub. This file becomes the VS Code Marketplace listing page.
It needs a real overview and screenshots before publishing.
Features
- Search sidebar — natural-language queries over indexed Lean declarations
- Multiple corpora — Mathlib, core, Batteries, and a local index of your own project
- Database management — download prebuilt indexes or build one for your workspace
Requirements
- A Lean 4 project (the extension activates on
lean-toolchain, lakefile.toml,
lakefile.lean, or .axiomatic)
That's it for marketplace installs: on first activation the extension sets
itself up automatically (see below). Developers and pip users can instead
point axSearchLean.pythonPath at their own install.
Automatic setup (marketplace builds)
On first activation the extension:
- downloads a pinned uv binary
(sha256-verified) into its private storage,
- uses it to install the pinned version of the
ax-assistant-release-staging
Python package (temporary staging name; final name TBD) — including a
self-contained Python; nothing on your machine is required or modified — and
- starts the search sidecar from that install.
Everything lives under VS Code's extension globalStorage directory;
uninstalling the extension and deleting that directory removes every trace.
Each extension release pins the exact package version it was tested with, so
extension updates from the Marketplace converge the Python side automatically.
If setup fails (e.g. offline), the status bar shows an error and
ax-search-lean: Retry setup runs it again.
Terminal / agent access (optional)
After the first successful start, the extension asks once whether to make the
ax-search-lean CLI available outside VS Code. Enabling it:
- symlinks
ax-search-lean (and the sidecar) into ~/.local/bin — existing
files there are never overwritten; only our own stale links are replaced —
and
- installs a Claude Code skill into the workspace's
.claude/skills/
(offering to add .claude/skills/ax-search-lean* to the repo's
.gitignore), so terminal agents can run Lean searches via the CLI. Skills
are per-workspace rather than user-global so they only appear in Lean
projects; each Lean workspace you open gets them on first activation, and
they re-sync when the extension updates.
Say "Not now" to be asked again next release, "Never" to opt out;
ax-search-lean: Enable terminal / agent access re-enables it any time.
On Windows the symlink step is currently skipped (the installed skill uses an
absolute path instead).
Commands
| Command |
Description |
ax-search-lean: Show Output |
Open the extension's output channel |
ax-search-lean: Retry setup |
Re-run the automatic setup (uv + Python package) |
ax-search-lean: Enable terminal / agent access |
Link the CLI into ~/.local/bin and install the Claude Code skill |
ax-search-lean: Check for search_db updates |
Check for newer prebuilt databases |
ax-search-lean: Fetch mathlib search_db |
Download the Mathlib index |
ax-search-lean: Fetch local search_db |
Fetch or build an index for this workspace |
Settings
| Setting |
Description |
axSearchLean.pythonPath |
Path to a Python interpreter with the package installed. Overrides the automatic setup; useful for development/editable installs. |
axSearchLean.packageSpec |
Development only: override the package requirement the bootstrap installs (e.g. a local wheel path). |
axSearchLean.searchLean.autoCheck |
Periodically check for search database updates |
axSearchLean.searchLean.checkIntervalHours |
How often to check |
axSearchLean.searchLean.autoFetch |
Download database updates without prompting |
TODO before publishing
- [ ] Screenshots / GIF of the search sidebar
- [ ] Install instructions for the Python package
- [ ] Note which corpora are available and how large they are
- [ ] Add
icon.png, and repository / bugs / keywords to package.json
License
AGPL-3.0-only.
