Axiomatic Octo

A Lean search toolkit connecting project-specific mathematical libraries to web, editor and agent workflows.

• Developer / Organization: Axiomatic AI
• Category: Related research systems & hosted services
• Purpose: Support Lean formalization with project-aware theorem search.
• Key features: Semantic search over projects and versioned dependencies, with web, editor and MCP interfaces. Separate from Axiom Math.
• Availability: Official project or research page; access varies
• License: Not verified in the linked source (source (opens in a new tab))
• Website / Source code: https://octo.axiomatic-ai.com/ (opens in a new tab)
• Version: No public software version found in the linked source
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01