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.

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

Set OPENROUTER_API_KEY in your environment or a project-root .env.secrets file, then run:

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

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.

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.