openprover

KO | EN

Minimalist Open Source Repository Search Engine

gitlite — search

#typescript #ai-agents #deepseek-harness #dsh-plugin #open-source #ai #cli #claude-code #windows #codex #developer-tools #dsh

★ 84 Open GitHub ↗

Automated Theorem Prover inspired by Aletheia. Claude Code for mathematicians.

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# OpenProver

![system_plot](https://raw.githubusercontent.com/Kripner/openprover/master/assets/openprover_system.png)

Theorem prover powered by language models.

A **planner** coordinates proof search by maintaining a whiteboard and repository, delegating focused tasks to parallel **workers**. Supports multiple LLM backends: Claude CLI, Mistral (Leanstral), GLM, OpenRouter-hosted models, and local models via vLLM.

## How it works

You give it a theorem statement (a `.md` file). A planner LLM maintains a **whiteboard** (terse mathematical scratchpad) and a **repository** of items (lemmas, observations, literature findings). Each step, the planner decides what to do: spawn workers to explore proof avenues, search literature, read/write repository items, or submit the proof.

Workers run in parallel (up to `-P` at a time), each focused on a single task. They can reference repository items via `[[wikilinks]]`. Results flow back to the planner, which updates the whiteboard and decides the next step.

With `--lean-project`, workers get access to **lean_verify** (compile Lean 4 code), **lean_store** (persist verified snippets across calls), and **lean_search** (search Mathlib/Lean declarations), enabling interactive formal proof development.

Modes:
- **Interactive** (default): see each step's plan, accept or give feedback
- **Autonomous** (`--autonomous`): runs hands-off until proof found or budget exhausted
- **Isolation** (default) / **No-isolation** (`--no-isolation`): by default, workers have no web access. With `--no-isolation`, the planner can use `literature_search` to find relevant papers and results online
- **Formal verification** (`--lean-project`): proof attempts are verified via `lake env lean`, workers can verify code and search Lean libraries

## Requirements

- Python 3.10+
- **Claude** (default): [Claude Code](https://docs.anthropic.com/en/docs/claude-code) (`claude` command on PATH)
- **Leanstral** (alternative): Mistral's Lean-specialized model; requires `MISTRAL_API_KEY` (get one at https://console.mistral.ai/)
- **GLM** (alternative): requires `GLM_API_KEY`
- **OpenRouter** (alternative): Kimi K2.5, MiniMax M2.5/M2.7; requires `OPENROUTER_API_KEY`
- **Local models** (alternative): any OpenAI-compatible server such as [vLLM](https://github.com/vllm-project/vllm); pass `--provider-url` to point at it

## Install

```bash
pip install openprover
```

Or from source:
```bash
git clone https://github.com/open-prover/openprover.git
cd openprover
python -m venv .venv && source .venv/bin/activate
pip install -e .
```

For Lean search support (optional):
```bash
openprover fetch-lean-data
```

## Usage

```bash
# Interactive mode (file argument = theorem)
openprover examples/sqrt2_irrational.md

# Autonomous with Opus, 2h time budget, 3 parallel workers
openprover --theorem examples/erdos_838.md --model opus --max-time 2h --autonomous -P 3

# Token budget instead of time
openprover --theorem examples/cauchy_schwarz.md --max-tokens 500000

# Resume an interrupted run (directory argument = run dir)
openprover runs/sqrt2-irrational-20260217-143012

# Use different models for planner and worker
openprover --theorem examples/cauchy_schwarz.md --planner-model opus --worker-model sonnet

# Enable web searches (disabled by default)
openprover --theorem examples/cauchy_schwarz.md --no-isolation

# Use Leanstral (Mistral's Lean-specialized model)
openprover --theorem examples/cauchy_schwarz.md --model leanstral

# Use GLM-5
openprover --theorem examples/cauchy_schwarz.md --model glm-5

# Use Kimi K2.5 via OpenRouter
openprover --theorem examples/cauchy_schwarz.md --model kimi-k2.5

# Use a local model (via vLLM)
openprover --theorem examples/infinite_primes.md --model minimax-m2.5 --provider-url http://localhost:8000

# Prove and formalize in Lean 4
openprover --theorem examples/addition.md \
  --lean-project ~/mathlib4 \
  --lean-theorem examples/addition.lean

# Formalize an existing proof
openprover --theorem examples/addition.md \
  --lean-project ~/mathlib4 \
  --lean-theorem examples/addition.lean \
  --proof runs/addition-20260223/PROOF.md
```

### Subcommands

| Command | Description |
|---------|-------------|
| `openprover <theorem.md>` | Run the prover (main command) |
| `openprover inspect [run_dir]` | Browse prompts and outputs from a run |
| `openprover fetch-lean-data` | Download Lean Explore search data and models |

### Options

| Flag | Default | Description |
|------|---------|-------------|
| `--model` | `sonnet` | Model for both planner and worker |
| `--planner-model` | | Override model for planner |
| `--worker-model` | | Override model for worker |
| `--max-time` | `4h` | Wall-clock time budget (e.g. `30m`, `2h`) |
| `--max-tokens` | | Output token budget (mutually exclusive with `--max-time`) |
| `--conclude-after` | `0.99` | Fraction of budget that triggers conclusion phase (0.9-1.0) |
| `--autonomous` | off | Run without human confirmation |
| `-P, --max-workers` | `1` | Max parallel workers per step |
| `--verifier` / `--no-verifier` | on | Run LLM verifier after each worker |
| `--effort` | auto | Claude reasoning effort: `low`, `medium`, `high`, `max` (max for opus, high for others) |
| `--isolation` / `--no-isolation` | on | Isolation disables web access; use `--no-isolation` to enable `literature_search` |
| `--history-budget` | auto | Char budget for planner history context |
| `--on-budget-out` | `exit` | Action when spending/rate limit hit: `backoff` or `exit` (Claude only) |
| `--on-rate-limited` | `backoff` | Action on HTTP 429: `backoff` or `exit` |
| `--lean-project` | | Path to Lean project with lakefile |
| `--lean-theorem` | | Path to THEOREM.lean (requires `--lean-project`) |
| `--proof` | | Path to existing PROOF.md (formalize-only mode) |
| `--lean-items` | auto | Allow saving .lean items to the repo (auto-enabled with `--lean-project`) |
| `--lean-worker-tools` | auto | Worker tool calls (lean_verify, lean_store, lean_search) via MCP/vLLM (auto-enabled with `--lean-project` + capable worker) |
| `--headless` | off | Non-interactive mode (logs to stdout, implies `--autonomous`) |
| `--verbose` | off | Show full LLM responses |
| `--read-only` | off | Inspect run without resuming |
| `--provider-url` | `http://localhost:8000` | Server URL for local models |
| `--answer-reserve` | `4096` | Tokens reserved for answer after thinking (local models) |

Available models: `sonnet`, `opus` (Claude); `leanstral` (Mistral, requires `MISTRAL_API_KEY`); `glm-5` (requires `GLM_API_KEY`); `kimi-k2.5`, `minimax-m2.5`, `minimax-m2.7` (OpenRouter, requires `OPENROUTER_API_KEY`). For local models, pass any model name supported by your server together with `--provider-url`.

### TUI controls

| Key | Action |
|-----|--------|
| `r` | Toggle reasoning trace |
| `i` | Show worker input (on worker tabs) |
| `w` | Toggle whiteboard view |
| `a` | Toggle autonomous mode |
| `Left/Right` | Switch between planner/worker tabs |
| `Up/Down` | Browse step history / navigate worker actions |
| `PgUp/PgDn` | Scroll content |
| `?` | Help overlay |

When confirming a step: Tab switches between accept/feedback, Enter confirms or opens detail view, Esc dismisses, `a` accepts and enters autonomous mode.

## Lean setup (for formal verification)

To use formal verification (`--lean-project`), you need [elan](https://github.com/leanprover/elan) (Lean version manager) installed. elan automatically fetches the right Lean toolchain.

Benchmarks like MiniF2F, PutnamBench, and ProofNet ship their own Lean projects with Mathlib dependencies. Build them once before running:

```bash
# MiniF2F
git clone https://github.com/google-deepmind/miniF2F.git
cd miniF2F
lake exe cache get   # download precompiled Mathlib oleans
lake build           # compile MiniF2F itself

# PutnamBench
git clone https://github.com/trishullab/PutnamBench.git
cd PutnamBench/lean4
lake exe cache get
lake build

# ProofNet (Lean 4.27.0 / Mathlib v4.27.0)
git clone https://github.com/kripner/proofnet.git
cd proofnet/ProofNet
lake exe cache get
lake build
```

Then point OpenProver at the project:

```bash
openprover --theorem thm.md --lean-project ./miniF2F --lean-theorem thm.lean
```

## Benchmarks

Scripts in `scripts/` run OpenProver against standard benchmarks:

```bash
# MiniF2F (fetches theorems from GitHub, uses local Lean project for verification)
python scripts/run_minif2f.py valid --model leanstral --repo-path ./miniF2F --max-time 10m --problem-parallelism 10
python scripts/run_minif2f.py test  --model leanstral --repo-path ./miniF2F --max-time 10m

# PutnamBench
python scripts/run_putnam.py --repo-path ./PutnamBench --model opus --max-time 2h --problem-parallelism 4

# ProofNet (loads problems from data/proofnet.jsonl, verifies against ProofNet/ lake project)
python scripts/run_proofnet.py valid --model leanstral --repo-path ./proofnet --max-time 10m --parallelism 10
python scripts/run_proofnet.py test  --model leanstral --repo-path ./proofnet --max-time 10m

# ProofBench
python scripts/run_proofbench.py --model leanstral --repo-path ./miniF2F --max-time 10m

# Run a single problem
python scripts/run_minif2f.py valid --problem mathd_algebra_182 --model leanstral --repo-path ./miniF2F
```

Use `--informal` to skip Lean verification (faster but scores are not meaningful).

## Planner actions

Each step, the planner chooses one action:

| Action | Description |
|--------|-------------|
| `spawn` | Delegate tasks to parallel workers |
| `literature_search` | Web-enabled search for relevant papers/results |
| `read_items` | Retrieve full content of repository items |
| `write_items` | Create, update, or delete repository items (lean items auto-verified) |
| `write_whiteboard` | Update the whiteboard without spawning workers |
| `read_theorem` | Re-read theorem statement(s) and any provided proof |
| `submit_proof` | Submit informal proof (terminates the session) |
| `submit_lean_proof` | Submit formal Lean proof (auto-verified with Lean) |

## Worker tools

When `--lean-project` is set with a tool-capable worker model, workers get access to:

| Tool | Description |
|------|-------------|
| `lean_verify(code)` | Compile Lean 4 code via `lake env lean`, returns OK or compiler errors |
| `lean_store(code)` | Persist a verified snippet; auto-prepended to subsequent `lean_verify` calls |
| `lean_search(query)` | Search Mathlib/Lean declarations by name or natural language query |

Tools are provided via MCP (Claude workers) or native tool calling (vLLM/OpenRouter/GLM workers). Actions are shown in the worker tab and can be browsed with arrow keys.

## Output

Each run creates a directory under `runs/`:

```
runs/<slug>-<timestamp>/
  THEOREM.md           - original theorem statement
  THEOREM.lean         - formal Lean statement (if provided)
  WHITEBOARD.md        - current whiteboard state
  PROOF.md             - final proof (if found)
  PROOF.lean           - formal Lean proof (if lean mode)
  DISCUSSION.md        - post-session analysis
  run_config.toml      - saved configuration (for resume)
  repo/                - repository items (lemmas, observations, etc.)
  steps/step_NNN/      - per-step planner decisions and worker results
  archive/calls/       - raw LLM call logs with cost/timing
```

All state lives on disk, so runs can be interrupted and resumed.

## Example theorems

The `examples/` directory has theorem statements at various difficulty levels:

| File | Difficulty |
|------|-----------|
| `sqrt2_irrational.md` | Easy |
| `infinite_primes.md` | Easy |
| `e_irrational.md` | Medium |
| `cauchy_schwarz.md` | Medium |
| `erdos_205.md` | Medium |
| `erdos_838.md` | Hard (open) |
| `collatz.md` | Harder (open) |

# Ideas

- Add modes where OpenProver also tries to 1) simplify a proof or make it nicer and 2) generalize a proof.
- In the `lean_verify` action, provide proof states to the planner.

# Cite

If you find OpenProver helpful in your research cite as:

```
@inproceedings{openprover,
  title     = {{OpenProver}: Agentic and Interactive Theorem Proving with {Lean 4}},
  author    = {Matěj Kripner and Milan Straka},
  booktitle = {19th Conference on Intelligent Computer Mathematics (CICM 2026)},
  year      = {2026},
  url       = {https://arxiv.org/abs/2607.09217}
}
```

openprover

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README