Provers

An automated theorem prover takes a formal statement in Lean and attempts to fill all sorry uses. OpenATP supports many theorem-provers ranging from general purpose coding agents to specialized theorem-proving agents.

Prover	ID	Skills	MCP	Paper	Source
Claude Code	claude	leanprover, lean4	✓	—	—
Codex	codex	leanprover	✓	—	GitHub
DeepSeek	deepseek	leanprover	✓	—	GitHub
Grok	grok	leanprover	✓	—	—
Muse Spark	spark	leanprover	✓	—	—
AxProverBase	axproverbase	—	✗	Requena et al. [6]	GitHub
Leanstral	leanstral	leanprover	✓	Mistral AI [9]	HuggingFace
Kimi Code	kimi	leanprover	✓	—	GitHub
Numina	numina	—	✓	Liu et al. [5]	GitHub
Aristotle	aristotle	—	—	Achim et al. [1]	—

Each prover is implemented as a subclass of AutomatedProver. There are multiple agent provers (AgentProver) that forward the task to a coding-agent harness (Harness). Agent harnesses are augmented with skills and MCP tooling.

• Skills. Most provers use the official Lean skills [8]. Claude Code additionally uses the lean4 skills packaged in the lean4 Claude Code plugin [3].

• MCP. The lean-lsp-mcp server [2] exposes the Lean language server as tools to provide rich feedback while iterating on proofs.