Axiomatic Octo

Axiomatic Octo is a swiss army knife for Lean (auto)formalization workflows. Today, it provides semantic search over your own projects and common dependencies such as Mathlib, Batteries, CSLib, and Physlib through a VS Code extension and Python CLI. The roadmap includes broader theorem-proving and knowledge-management tools.

Install

VS Code (recommended): install Axiomatic Octo from the Marketplace and open a Lean project. The extension completes setup on first activation.

Hosted project indexing requires a GitHub repository. The extension identifies it from the Git origin remote and supports SSH host aliases when the remote path uses the standard owner/repository form.

CLI only:

uv tool install axiomatic-octo

To build your own search index, install the optional dependencies:

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

Quickstart

No account, no keys:

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

octo search fetch downloads the shared corpora (mathlib and friends) anonymously, under a global ceiling of 1,000 anonymous downloads per day. It fetches this project's own local.db too, if the repository is registered for search and the Axiomatic search GitHub App is installed for its owner; without that there is nothing published for the project itself to download.

octo search query embeds the query through the Axiomatic server, which serves 60 anonymous queries per hour per IP address. That is a rolling window, not a daily allowance. Set OPENROUTER_API_KEY in your environment or a project-root .env.secrets file to spend your own provider key instead. An Axiomatic API key (OCTO_SERVER_TOKEN) is what buys reranking, private repositories, building your own index, and rate limits of your own.

Use octo search status to check installed databases and updates. Local index creation is available through octo search index when the optional dependencies are installed.

Axiomatic hosts project databases by default. Repositories that already build a search-lean-db workflow artifact can set search_lean.db_source to workflow. Octo uses only the selected source and does not fall back.

Agents

Octo includes a workspace-scoped Claude Code skill that lets agents search Lean declarations through the CLI. After the VS Code extension starts successfully, enable terminal and agent access when prompted. You can also run Octo: Enable terminal / agent access from the Command Palette. The extension installs the skill under .claude/skills/, offers to add .claude/skills/octo* to .gitignore, and keeps the skill synchronized when Octo updates.

Development

uv sync
pnpm install

uv run pytest
uv run ruff check .
pnpm --filter axiomatic-octo run test

To run the extension from source, open the repository in VS Code and launch Run Search Extension (isolated). After changing src/axiomatic_octo/protocol.py, regenerate the TypeScript bindings with:

pnpm --filter axiomatic-octo run protocol:codegen

License

AGPL-3.0-only. See LICENSE.