Provers

A prover is a candidate generator: it takes a ProofTask and produces completed Lean files. The base AutomatedProver owns the shared lifecycle — generate, then verify in the sandbox — so every prover gets the same final check for free.

Prover

Spec

Generation

Credential

Claude Code

agent

AgentProver on the Claude Code CLI

CLAUDE_CODE_OAUTH_TOKEN

Codex

agent:codex

AgentProver on the Codex CLI (OpenAI)

~/.codex (OAuth)

OpenCode

agent:opencode

AgentProver on the OpenCode CLI (any provider)

<PROVIDER>_API_KEY

AxProver

agent:axprover

AgentProver driving ax-prover-base

ANTHROPIC / OPENAI / GOOGLE_API_KEY

Vibe / Leanstral

vibe

AgentProver on Mistral Vibe’s lean agent

MISTRAL_API_KEY

NuminaProver

numina

AgentProver (Claude) + Numina assets + round loop

harness + helper API keys

AristotleProver

aristotle

Harmonic’s hosted Aristotle API

ARISTOTLE_API_KEY

The Claude Code, Codex, OpenCode, AxProver, and Vibe provers are all the same AgentProver composed with a different Harness; Spec is the get_prover() registry name. Every prover subclasses AutomatedProver and funnels its output through the shared Verifier.

How the agent provers work

An AgentProver composes two concerns:

  • a Harness — the agent concern: launch script, credential forwarding, and output parsing (one per harness page below); and

  • a ComputeBackend — the compute concern: where the agent runs, with Lean+Mathlib and the lean-lsp-mcp server.

prove stages the project into the workdir, lets the agent fill the sorrys in place, then diffs the .lean files against the staged originals to report what changed. The shared Verifier does the final compile / sorry / axiom check. Configuration fields are documented under AgentProverConfig in the provers reference.