Axiomatic Octo

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

Features

Search Lean declarations using natural language
Search your local project and common dependencies, e.g., Mathlib, Batteries, CSLib, and Physlib
Download prebuilt search databases and keep them updated
Use the same search tools from coding agents and the terminal

Get started

Install Axiomatic Octo from the Marketplace and open a Lean project. The extension completes setup on first activation. Open the Octo sidebar to search.

Self-hosted

To build your project search database in your own GitHub Actions environment, install the Octo workflow in your repository and add your model-provider API keys as repository secrets. Octo can download the resulting workflow artifact for use in the extension.

Agents

After setup, enable terminal and agent access when prompted, or run Octo: Enable terminal / agent access from the Command Palette. This exposes the octo CLI and offers to install a workspace-scoped Claude Code skill under .claude/skills/ in each repository. Installing requires repository-specific consent and, for Git repositories, also adds .claude/skills/octo* to .gitignore. You can decline one repository or disable future skill-install offers. The extension keeps skills synchronized only in repositories you approve.

Commands

Command	Description
`Octo: Show Output`	Open the extension output
`Octo: Retry setup`	Retry automatic setup
`Octo: Enable terminal / agent access`	Install the CLI link and ask about the agent skill for this repository
`Octo: Check for search_db updates`	Check for database updates

License

AGPL-3.0-only. See LICENSE.

Axiomatic Octo

Axiomatic_AI

Axiomatic Octo

Features

Get started

Self-hosted

Agents

Commands

License