AxProverBase

A minimal Lean proving agent built around iterative proposals, compilation, review and memory.

• Developer / Organization: Axiomatic AI; Borja Requena, Austin Letson and collaborators
• Category: Open-source formalization & proving
• Purpose: Provide a minimal general-model Lean proving agent.
• Key features: Iterative proposing, compilation, proof review and memory, with library-search tools. Separate from Axiom Math.
• Availability: Open-source software; AGPL-3.0
• License: AGPL-3.0 (source (opens in a new tab))
• Website / Source code: https://github.com/Axiomatic-AI/ax-prover-base (opens in a new tab)
• Version: GitHub release v0.1.1
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01