Skip to content

Axiomatic Octo

Axiomatic Octo logo

Axiomatic Octo is a toolkit for Lean formalization workflows. Octo Search lets you search semantically for declarations across Mathlib, core, Batteries, and your own Lean projects at once.

Octo gives every branch of your Lean repository its own search index, both for your own own code and its dependencies, whether you work in VS Code, the CLI, or with a coding agent.

Status: alpha

Stable enough for daily use; APIs and file formats may still shift. This manual tracks main.

Octo Search product screenshot placeholder

Try it without installing anything

Search the shared corpora from your browser at octo.axiomatic-ai.com/search. Searching your own Lean project is what the VS Code extension and the CLI add.

Start here

  • Install

    Installing the CLI and extension, and configuring API keys.

  • Web search

    Query the shared corpora in your browser, nothing to install.

  • Set up search on your repo

    A walkthrough of the setup checklist, from sign-in to your first query.

  • Agents and MCP

    Wiring Claude Code, Codex, and Cursor to Octo's two MCP servers: octo-mcp, over your own project, and hosted Octo Search, over public corpora with nothing to install.

  • CLI reference

    Every command's --help, generated from the installed CLI.

  • Configuration

    Config layering, model aliases, and tuning knobs.

The pipeline

Each corpus has a search database under <project>/.axiomatic/search_lean/: a SQLite file with a sqlite-vec vector index. Databases are either downloaded prebuilt or built locally from a Lean project.

flowchart LR
    REL["GitHub Releases<br/>(mathlib, core, ...)"] -->|fetch| DB
    CI["your project's CI artifacts"] -->|fetch --target local| DB
    LEAN["your Lean project"] -->|index| DB
    DB[".axiomatic/search_lean/<br/>*.db"]
    DB -->|query| YOU([results])

Indexing extracts Lean declarations with lean-extract (inspired by jixia and doc-gen4), describes each one informally with an LLM, and embeds the descriptions with an open embedding model. Queries embed your question the same way and rank declarations by similarity.

Getting help