Skip to content

Install Axiomatic Octo

Nothing to install if you only want to search the shared corpora: use octo.axiomatic-ai.com/search. Install Octo to search your own Lean project, and to search from your editor, terminal, or a coding agent.

  1. Install Axiomatic Octo from the VS Code Marketplace.
  2. Open a Lean project folder in VS Code.
  3. Open the Octo sidebar and follow the setup checklist.
  4. Search your project and its dependencies from the Octo Search panel.

On first activation, the extension installs the Octo runtime and guides you through setup. See Set up search on your repo for a screenshot-by-screenshot walkthrough.

Terminal and agent access

The extension can also expose the octo CLI and install a workspace-scoped Claude Code skill. After setup, accept the prompt or run Octo: Enable terminal / agent access from the Command Palette.

Octo asks for permission separately in each repository before installing the skill under .claude/skills/.

Octo also provides two MCP servers for coding agents. octo-mcp searches this project, including your own unpublished code; VS Code configures it for you, and Claude Code, Codex, and Cursor each take one line of configuration. Hosted Octo Search searches prebuilt public corpora and needs nothing installed at all, not even this package: it is a URL. See Agents and MCP.

Check the installation

Open the Octo sidebar and run a search. If setup does not complete:

  • Run Octo: Retry setup from the Command Palette.
  • Run Octo: Show Output to see the setup and sidecar logs.

CLI only

Install the package as a command-line tool with uv:

uv tool install axiomatic-octo

This installs octo, octo-sidecar, and octo-mcp on your PATH. Verify the installation:

octo --help
octo search --help

Choose how Octo accesses models

Fetching and querying need no key at all. octo search fetch downloads the shared corpora anonymously, under a global ceiling of 1,000 anonymous downloads per day, and query embeddings go through the Axiomatic server at 60 anonymous queries per hour per IP address (a rolling window, not a daily allowance).

Reranking, private repositories, building your own index, and rate limits of your own are what the credentials below are for.

Route query embeddings and reranking through the Axiomatic server by setting your Axiomatic API key:

export OCTO_SERVER_TOKEN=...

Reranking is the visible difference: without a credential the query returns vector-ranked results and says so. The same token authorizes search databases for your private repositories, lifts the shared anonymous rate limits, and is required to build an index of your own.

The VS Code extension supplies this credential automatically after you sign in.

Send query embeddings and reranking directly to OpenRouter by setting your own key:

export OPENROUTER_API_KEY=...

You can instead store the key in .env.secrets at the root of your Lean project:

# .env.secrets
OPENROUTER_API_KEY=...

Add .env.secrets to .gitignore; never commit API keys.

Other credentials

Building a local index may require additional provider keys if you override the default models. See Configuration.

From a Lean project:

cd my-lean-project
octo search fetch
octo search query "self-adjoint operator is symmetric"

Use octo search status to see which project and dependency databases are installed and whether updates are available.

Build a local search index

Querying and fetching use the standard installation. To build a search index yourself, install the optional indexing dependencies:

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

Then run octo search index from your Lean project. Indexing can make many model-provider calls, so run octo search index --dry-run to estimate the cost before starting a large build.

Next

Set up search on your repo

Agents and MCP