### Install OpenProver from Source

Source: https://github.com/kripner/openprover/blob/master/README.md

Install OpenProver from its source code. This involves cloning the repository, setting up a virtual environment, and installing the package in editable mode.

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

--------------------------------

### Run OpenProver on Theorem Files

Source: https://context7.com/kripner/openprover/llms.txt

Command-line examples for running OpenProver against various theorem files, specifying difficulty levels or advanced options.

```bash
# Run against each difficulty level
openprover examples/sqrt2_irrational.md    # Easy
openprover examples/infinite_primes.md     # Easy
openprover examples/e_irrational.md        # Medium
openprover examples/cauchy_schwarz.md      # Medium
openprover examples/erdos_205.md           # Medium
openprover --theorem examples/erdos_838.md --autonomous --max-time 4h  # Hard
openprover --theorem examples/collatz.md   --autonomous --max-time 4h  # Very Hard (open)
```

--------------------------------

### Prove and Formalize in Lean 4 Simultaneously

Source: https://context7.com/kripner/openprover/llms.txt

Run OpenProver to both find an informal proof and formalize it in Lean 4. Requires a Lean project setup and a `.lean` file with `sorry` placeholders. Workers gain access to Lean tools.

```bash
openprover --theorem examples/addition.md \
  --lean-project ./miniF2F \
  --lean-theorem examples/addition.lean \
  --autonomous --max-time 1h
```

--------------------------------

### Lean Theorem File Example

Source: https://context7.com/kripner/openprover/llms.txt

Example of a Lean 4 theorem file, including necessary imports and a theorem statement with a 'sorry' placeholder for the proof body.

```lean
-- examples/addition.lean
import Mathlib

abbrev add_solution : ℕ := sorry

theorem add :
    42 + 24 = add_solution := by
  sorry

```

--------------------------------

### Install OpenProver with pip

Source: https://github.com/kripner/openprover/blob/master/README.md

Install the OpenProver package using pip. This is the recommended method for most users.

```bash
pip install openprover
```

--------------------------------

### Inspect and Resume OpenProver Runs

Source: https://context7.com/kripner/openprover/llms.txt

Command-line examples for interacting with OpenProver run directories, including inspecting state and resuming interrupted processes.

```bash
# Inspect any run interactively (read-only TUI)
openprover inspect runs/sqrt2-irrational-20260217-143012

# Resume an in-progress run (restores whiteboard + step history)
openprover runs/sqrt2-irrational-20260217-143012

# Override budget on resume
openprover runs/sqrt2-irrational-20260217-143012 --max-time 1h
```

--------------------------------

### OpenProver CLI Entry Point

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

The main entry point for the OpenProver CLI. It handles argument parsing, prover initialization, TUI setup, signal handling, and cost reporting.

```python
cli.py          Parse args, setup TUI, run prover, print cost
prover.py       Planner loop, step dispatch, action handlers, Repo
prompts.py      All prompt templates, TOML parser, actions enum
budget.py       Budget tracking (token or time limits)
inspect.py      Read-only run browser
llm/
  _base.py      Shared helpers: Interrupted, StreamingUnavailable, archive(), error detection
  claude.py     LLMClient - Claude CLI wrapper (default backend)
  mistral.py    MistralClient - Mistral Conversations API (Leanstral)
  glm.py        GLMClient - Z.ai OpenAI-compatible API (GLM-5)
  openrouter.py OpenRouterClient - OpenRouter API (Kimi K2.5, MiniMax M2.5/M2.7)
  hf.py         HFClient - local OpenAI-compatible servers (vLLM, serve_hf.py)
lean/
  core.py       Lean 4 integration: parsing, assembly, verification
  data.py       Lean Explore data management (fetch, availability checks)
  mcp_server.py MCP server exposing lean_verify, lean_store, lean_search tools
  tools.py      Tool definitions for vLLM native tool calling, execute_worker_tool()
tui/
  tui.py        Full-screen interactive TUI (ANSI scroll regions, tabs, streaming)
  headless.py   Non-interactive TUI (logs to stdout/stderr)
  _render.py    Terminal rendering, ANSI coloring
  _steps.py     Step/turn display logic
  _stream.py    Real-time streaming text updates
  _input.py     User input handling (keyboard, confirmation UI)
  _nav.py       Navigation state (tab switching, history)
  _tabs.py      Tab management (planner vs worker views)
  _text.py      Text utilities (wrapping, formatting)
  _colors.py    ANSI color/style definitions
  _types.py     Type definitions for TUI state
```

--------------------------------

### Slug Format Example

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

An example illustrating the format of the 'slug' used in run directory naming conventions. It is derived from the theorem name, lowercased, and with non-alphanumeric characters replaced by hyphens.

```text
sqrt2-irrational-20260220-143706
```

--------------------------------

### Fetch Lean Data and Dependencies in Python

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

Checks for necessary LeanExplore packages and data, installs them if missing, and fetches search data. This is called automatically or via a command-line interface.

```python
def is_lean_data_available():
    """Checks for lean-explore package, torch, sentence-transformers, and fetched data files."""
    pass

def fetch_lean_data():
    """Installs missing dependencies (lean-explore, torch CPU, sentence-transformers), fetches search data via `lean-explore data fetch`, and pre-downloads the embedding model."""
    pass
```

--------------------------------

### Markdown Theorem Statement Example

Source: https://context7.com/kripner/openprover/llms.txt

Example of a theorem statement in a Markdown file, including a natural language description and mathematical claim.

```markdown
<!-- examples/sqrt2_irrational.md -->
Prove that $\sqrt{2}$ is irrational.

That is, prove that there is no rational number $p/q$ (with $p, q$ integers, $q \neq 0$) such that $(p/q)^2 = 2$.
```

```markdown
<!-- examples/infinite_primes.md -->
Prove that there are infinitely many prime numbers.

That is, for every positive integer $n$, there exists a prime $p > n$.
```

--------------------------------

### Fetch Lean Search Data

Source: https://context7.com/kripner/openprover/llms.txt

Installs necessary packages and downloads Lean 4 declaration embeddings and FAISS index for semantic search. Can be triggered programmatically or via CLI.

```python
from openprover.lean.data import is_lean_data_available, fetch_lean_data

# Check if search data is ready (fast, no network)
if not is_lean_data_available():
    print("Lean search data not available — fetching...")
    success = fetch_lean_data()
    # Installs: lean-explore, torch (CPU), sentence-transformers
    # Downloads: lean_explore.db (~400k declarations), FAISS index,
    #            Qwen3-Embedding-0.6B, Qwen3-Reranker-0.6B (GPU only)
    if success:
        print("Ready.")
    else:
        print("Fetch failed — lean_search will be unavailable")
else:
    print("Lean search data is available.")

# Or use the CLI subcommand:
# openprover fetch-lean-data
```

--------------------------------

### Run OpenProver with Kimi K2.5 via OpenRouter

Source: https://github.com/kripner/openprover/blob/master/README.md

Use the Kimi K2.5 model through OpenRouter for OpenProver.

```bash
openprover --theorem examples/cauchy_schwarz.md --model kimi-k2.5
```

--------------------------------

### Run OpenProver with Kimi K2.5 via OpenRouter

Source: https://context7.com/kripner/openprover/llms.txt

Utilize the Kimi K2.5 model hosted on OpenRouter. Requires the OPENROUTER_API_KEY environment variable to be set.

```bash
OPENROUTER_API_KEY=sk-... openprover \
  --theorem examples/infinite_primes.md \
  --model kimi-k2.5
```

--------------------------------

### Run ProofBench

Source: https://context7.com/kripner/openprover/llms.txt

Executes problems from the ProofBench benchmark, specifying the model, repository path, and maximum time.

```bash
python scripts/run_proofbench.py \
  --model leanstral \
  --repo-path ./miniF2F \
  --max-time 10m
```

--------------------------------

### Clone and Build PutnamBench Project

Source: https://github.com/kripner/openprover/blob/master/README.md

Clone the PutnamBench repository and build its Lean project. This is necessary for running benchmarks that utilize PutnamBench for formal verification.

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

--------------------------------

### Run OpenProver with Local vLLM Server

Source: https://context7.com/kripner/openprover/llms.txt

Connect to a locally running LLM server via vLLM. Specify the provider URL for the server.

```bash
openprover --theorem examples/infinite_primes.md \
  --model minimax-m2.5 \
  --provider-url http://localhost:8000
```

--------------------------------

### Run OpenProver with Token Budget

Source: https://github.com/kripner/openprover/blob/master/README.md

Execute OpenProver using a maximum token count as the budget, instead of a time limit.

```bash
openprover --theorem examples/cauchy_schwarz.md --max-tokens 500000
```

--------------------------------

### Run OpenProver with Token Budget

Source: https://context7.com/kripner/openprover/llms.txt

Use this command to limit the prover's execution based on a token budget rather than wall-clock time. Useful for controlling LLM costs.

```bash
openprover --theorem examples/cauchy_schwarz.md \
  --max-tokens 500000 \
  --autonomous
```

--------------------------------

### Fetch Lean Data for OpenProver

Source: https://github.com/kripner/openprover/blob/master/README.md

Download necessary data for Lean search support within OpenProver. This is an optional step.

```bash
openprover fetch-lean-data
```

--------------------------------

### OpenProver with Lean Verification

Source: https://github.com/kripner/openprover/blob/master/README.md

Command to run OpenProver with Lean formal verification enabled. It specifies the theorem file, Lean project path, and the Lean theorem to verify.

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

--------------------------------

### Prove and Formalize in Lean 4 with OpenProver

Source: https://github.com/kripner/openprover/blob/master/README.md

Use OpenProver to generate a proof and formalize it in Lean 4, specifying the Lean project directory and the target Lean theorem file.

```bash
openprover --theorem examples/addition.md \
  --lean-project ~/mathlib4 \
  --lean-theorem examples/addition.lean
```

--------------------------------

### Run ProofBench Benchmark

Source: https://github.com/kripner/openprover/blob/master/README.md

Execute the ProofBench benchmark script. This command specifies the model, repository path, and time limit.

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

--------------------------------

### Formalize an Existing Proof with OpenProver

Source: https://github.com/kripner/openprover/blob/master/README.md

Load an existing proof from a markdown file and formalize it in Lean 4 using OpenProver. Requires specifying the Lean project and target Lean theorem file.

```bash
openprover --theorem examples/addition.md \
  --lean-project ~/mathlib4 \
  --lean-theorem examples/addition.lean \
  --proof runs/addition-20260223/PROOF.md
```

--------------------------------

### Clone and Build MiniF2F Project

Source: https://github.com/kripner/openprover/blob/master/README.md

Clone the MiniF2F repository and build its Lean project. This is a prerequisite for running benchmarks that use MiniF2F for formal verification.

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

--------------------------------

### Run OpenProver with Different Planner and Worker Models

Source: https://github.com/kripner/openprover/blob/master/README.md

Configure OpenProver to use distinct language models for the planner and the workers.

```bash
openprover --theorem examples/cauchy_schwarz.md --planner-model opus --worker-model sonnet
```

--------------------------------

### Run OpenProver with Split Planner and Worker Models

Source: https://context7.com/kripner/openprover/llms.txt

Configure OpenProver to use different LLM models for planning and execution. This allows for specialized roles, e.g., a powerful planner with a faster worker.

```bash
openprover --theorem examples/cauchy_schwarz.md \
  --planner-model opus \
  --worker-model sonnet \
  --autonomous
```

--------------------------------

### Run OpenProver with a Local Model

Source: https://github.com/kripner/openprover/blob/master/README.md

Connect OpenProver to a local language model server, such as one provided by vLLM, by specifying the provider URL.

```bash
openprover --theorem examples/infinite_primes.md --model minimax-m2.5 --provider-url http://localhost:8000
```

--------------------------------

### Run MiniF2F Benchmark (Test)

Source: https://github.com/kripner/openprover/blob/master/README.md

Execute the MiniF2F benchmark script for testing. This command specifies the model, repository path, and time limit.

```python
python scripts/run_minif2f.py test  --model leanstral --repo-path ./miniF2F --max-time 10m
```

--------------------------------

### Run PutnamBench Benchmark

Source: https://github.com/kripner/openprover/blob/master/README.md

Execute the PutnamBench benchmark script. This command specifies the repository path, model, time limit, and problem parallelism.

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

--------------------------------

### Successful Tool Call with Short Instructions

Source: https://github.com/kripner/openprover/blob/master/scripts/repro_leanstral_tools.md

When using short instructions, the API response correctly includes a 'function.call' entry, indicating the model is attempting to use the provided tool.

```json
{
  "outputs": [
    {
      "type": "message.output",
      "role": "assistant",
      "content": [{"type": "thinking", "thinking": [{"type": "text", "text": "The user wants me to call the add tool with a=2 and b=3."}]}
    },
    {
      "type": "function.call",
      "name": "add",
      "arguments": "{\"a\": 2, \"b\": 3}"
    }
  ]
}
```

--------------------------------

### Run Minif2f Problem

Source: https://context7.com/kripner/openprover/llms.txt

Executes a specific problem from the minif2f benchmark using a specified model and repository path.

```bash
python scripts/run_minif2f.py valid \
  --problem mathd_algebra_182 \
  --model leanstral \
  --repo-path ./miniF2F
```

```bash
python scripts/run_minif2f.py valid \
  --model sonnet \
  --repo-path ./miniF2F \
  --informal
```

--------------------------------

### Formalize an Existing Informal Proof in Lean 4

Source: https://context7.com/kripner/openprover/llms.txt

Use this command to formalize a theorem in Lean 4, skipping the informal proof search phase. Requires a path to an existing informal proof file.

```bash
openprover --theorem examples/addition.md \
  --lean-project ./miniF2F \
  --lean-theorem examples/addition.lean \
  --proof runs/addition-20260223/PROOF.md \
  --autonomous --max-time 45m
```

--------------------------------

### OpenProver Budget Tracking

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

Manages session budgets using either time or token limits. The `Budget` class tracks progress and provides status for planner pacing.

```python
budget.py       Budget tracking (token or time limits)
```

--------------------------------

### Run OpenProver with Leanstral Model

Source: https://context7.com/kripner/openprover/llms.txt

Execute OpenProver using Leanstral, Mistral's model fine-tuned for Lean. Requires the MISTRAL_API_KEY environment variable to be set.

```bash
MISTRAL_API_KEY=sk-... openprover \
  --theorem examples/cauchy_schwarz.md \
  --model leanstral
```

--------------------------------

### Run OpenProver with Web Search Enabled

Source: https://github.com/kripner/openprover/blob/master/README.md

Enable web search capabilities for OpenProver workers. This is disabled by default.

```bash
openprover --theorem examples/cauchy_schwarz.md --no-isolation
```

--------------------------------

### Run OpenProver in Autonomous Mode with Time Budget

Source: https://context7.com/kripner/openprover/llms.txt

This command runs the prover autonomously until a proof is found or the specified time budget is exhausted. Suitable for automated proof searches.

```bash
openprover --theorem examples/erdos_838.md \
  --model opus \
  --max-time 2h \
  --autonomous \
  -P 3
```

--------------------------------

### Run Directory Structure

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

This outlines the typical file structure of a completed run directory for OpenProver. It includes theorem statements, proof artifacts, configuration files, and archived LLM calls.

```text
runs/<slug>-<timestamp>/
  THEOREM.md                   - immutable copy of input
  THEOREM.lean                 - formal Lean statement (if --lean-theorem)
  WHITEBOARD.md                - latest whiteboard state (enables resume)
  PROOF.md                     - written only if proof found
  PROOF.lean                   - formal Lean proof (if lean mode)
  DISCUSSION.md                - post-session analysis
  run_config.toml              - saved run configuration (for resume)
  repo/
    *.md                       - repository items (lemmas, observations, etc.)
  steps/
    step_001/
      planner.toml             - planner's TOML decision
      workers/
        task_0.md              - worker task description
        result_0.md            - worker output
        worker_0_call.json     - archived LLM call
    step_002/...
  archive/
    calls/
      call_001.json            - full LLM call record
```

--------------------------------

### Run MiniF2F Benchmark (Valid)

Source: https://github.com/kripner/openprover/blob/master/README.md

Execute the MiniF2F benchmark script for validation. This command specifies the model, repository path, time limit, and problem parallelism.

```python
python scripts/run_minif2f.py valid --model leanstral --repo-path ./miniF2F --max-time 10m --problem-parallelism 10
```

--------------------------------

### Local vLLM / OpenAI-compatible LLM Client

Source: https://context7.com/kripner/openprover/llms.txt

Connects to any OpenAI-compatible HTTP server, such as vLLM. Handles streaming via SSE, reasoning extraction, and tool calling. Cost is 0.0 for local models.

```python
from pathlib import Path
from openprover.llm.hf import HFClient, MODEL_CONTEXT_LENGTHS

# Register a custom model context length before instantiating
MODEL_CONTEXT_LENGTHS["my-model"] = 32_768

client = HFClient(
    model="my-model",
    archive_dir=Path("runs/my-run/archive"),
    base_url="http://localhost:8000",
    answer_reserve=4096,   # tokens reserved for answer after thinking
    vllm=True,
)

# Basic inference call
response = client.call(
    prompt="Give a sketch proof that e is irrational.",
    system_prompt="You are an expert mathematician.",
    stream_callback=lambda text: print(text, end="", flush=True),
)
print(response["result"])    # answer text (after </think> boundary)
print(response["thinking"])  # chain-of-thought (inside <think>...</think>)
```

--------------------------------

### Run OpenProver in Interactive Mode

Source: https://github.com/kripner/openprover/blob/master/README.md

Execute OpenProver in interactive mode, providing a theorem statement as a markdown file. This is the default mode.

```bash
openprover examples/sqrt2_irrational.md
```

--------------------------------

### Run Putnam Benchmark

Source: https://context7.com/kripner/openprover/llms.txt

Executes problems from the PutnamBench competition, allowing for parallel processing and specifying maximum time.

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

--------------------------------

### Run OpenProver with Leanstral Model

Source: https://github.com/kripner/openprover/blob/master/README.md

Utilize Leanstral, Mistral's Lean-specialized model, for OpenProver tasks.

```bash
openprover --theorem examples/cauchy_schwarz.md --model leanstral
```

--------------------------------

### No Tool Call with Long Instructions

Source: https://github.com/kripner/openprover/blob/master/scripts/repro_leanstral_tools.md

With longer instructions, the tool call is omitted, and the model provides a generic text response, ignoring the user's request to use the tool.

```json
{
  "outputs": [
    {
      "type": "message.output",
      "role": "assistant",
      "content": "Got it! I'm here to help with math problems, calculations, and explanations."
    }
  ]
}
```

--------------------------------

### Log Step Completion in OpenProver

Source: https://context7.com/kripner/openprover/llms.txt

Logs the completion of a step in the OpenProver process, including the step number, action, and a summary.

```python
idx = tui.step_complete(
    step_num=3,
    action="spawn",
    summary="Dispatched 2 contradiction workers",
)
```

--------------------------------

### OpenProver Output Directory Structure

Source: https://github.com/kripner/openprover/blob/master/README.md

Details the directory structure created by each OpenProver run. All state is persisted on disk, allowing for interrupted and resumed runs.

```bash
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

```

--------------------------------

### Run MiniF2F Benchmark Test Split

Source: https://context7.com/kripner/openprover/llms.txt

Execute the MiniF2F test split benchmark. This command is similar to the validation split but targets the test set.

```python
python scripts/run_minif2f.py test \
  --model leanstral \
  --repo-path ./miniF2F \
  --max-time 10m
```

--------------------------------

### Initialize Headless TUI

Source: https://context7.com/kripner/openprover/llms.txt

Sets up the non-interactive logging interface for batch or CI environments. Logs to stdout and stderr.

```python
from openprover.tui.headless import HeadlessTUI

tui = HeadlessTUI()
tui.setup(
    theorem_name="sqrt2_irrational",
    work_dir="runs/sqrt2-20260217",
    model_name="sonnet",
)
```

--------------------------------

### OpenAI Function Calling Tools for Lean in Python

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

Defines tool specifications for Lean verification, storage, and search in OpenAI function-calling format. Includes a function to execute these tools.

```python
WORKER_TOOLS = [
    # tool specs for lean_verify, lean_store, lean_search
]

def execute_worker_tool():
    """Dispatches tool calls and manages per-worker persistent stores."""
    pass
```

--------------------------------

### Lean Theorem Parsing and Proof Assembly in Python

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

Parses Lean 4 theorem files, identifies 'sorry' positions, and assembles proofs by replacing 'sorry' placeholders with provided code blocks.

```python
class LeanTheorem:
    # ... (implementation details omitted for brevity)

    def assemble_proof(self, replacements, context):
        """Replaces each sorry with its corresponding block (in reverse order to preserve offsets), injects optional context after preamble.

        Validates: correct count, no `import` in injected code.
        """
        pass
```

--------------------------------

### LLM Client Implementations

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

Shared helpers and specific client implementations for various Large Language Models, including Claude, Mistral, GLM, OpenRouter, and Hugging Face models.

```python
llm/_base.py      Shared helpers: Interrupted, StreamingUnavailable, archive(), error detection
llm/claude.py     LLMClient - Claude CLI wrapper (default backend)
llm/mistral.py    MistralClient - Mistral Conversations API (Leanstral)
llm/glm.py        GLMClient - Z.ai OpenAI-compatible API (GLM-5)
llm/openrouter.py OpenRouterClient - OpenRouter API (Kimi K2.5, MiniMax M2.5/M2.7)
llm/hf.py         HFClient - local OpenAI-compatible servers (vLLM, serve_hf.py)
```

--------------------------------

### Run Single MiniF2F Problem

Source: https://github.com/kripner/openprover/blob/master/README.md

Execute the MiniF2F benchmark script for a single problem. This command specifies the problem name, model, repository path, and time limit.

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

--------------------------------

### Run OpenProver with GLM-5 Model

Source: https://github.com/kripner/openprover/blob/master/README.md

Configure OpenProver to use the GLM-5 model.

```bash
openprover --theorem examples/cauchy_schwarz.md --model glm-5
```

--------------------------------

### Inspect OpenProver Run Data

Source: https://github.com/kripner/openprover/blob/master/README.md

Browse the prompts and outputs from a previous OpenProver run by providing the run directory.

```bash
openprover inspect [run_dir]
```

--------------------------------

### Worker Tools: lean_verify, lean_store, lean_search

Source: https://context7.com/kripner/openprover/llms.txt

Tools for workers: `lean_verify` compiles Lean 4 code, `lean_store` persists verified lemmas, and `lean_search` is also available. These are delivered via FastMCP or OpenAI function calling.

```python
# lean_verify: compile Lean 4 code, returns "OK - no errors" or error text
result = lean_verify("""
import Mathlib
theorem add : 1 + 1 = 2 := by norm_num
""")
# "OK - no errors"

# lean_store: persist a verified lemma; auto-prepended to future lean_verify
result = lean_store("""
import Mathlib
lemma my_lemma : ∀ n : ℕ, n + 0 = n := fun n => Nat.add_zero n
""")
# "OK - stored.\n\nCurrent store:\n```lean\n...\n```"
```

--------------------------------

### Run OpenProver in Autonomous Mode with Custom Settings

Source: https://github.com/kripner/openprover/blob/master/README.md

Run OpenProver autonomously with a specified model (Opus), a time budget, and a set number of parallel workers.

```bash
openprover --theorem examples/erdos_838.md --model opus --max-time 2h --autonomous -P 3
```

--------------------------------

### Multi-turn Tool Calling with WORKER_TOOLS

Source: https://context7.com/kripner/openprover/llms.txt

Demonstrates multi-turn chat interactions using predefined worker tools. Requires `WORKER_TOOLS` to be imported.

```python
from openprover.lean.tools import WORKER_TOOLS

messages = [{"role": "user", "content": "Verify this Lean code: ..."}]
final_response = client.chat(
    messages=messages,
    system_prompt="You are a Lean 4 expert.",
    tools=WORKER_TOOLS,
    tool_executor=lambda name, args: ("OK", "ok"),
    stream_callback=lambda text: None,
)
print(final_response["result"])
```

--------------------------------

### Run OpenProver in Headless CI/Batch Mode

Source: https://context7.com/kripner/openprover/llms.txt

Execute OpenProver in headless mode for CI or batch processing. Output is directed to stdout, and no TUI is displayed. Returns '[result] proved', '[result] not_proved', or '[result] rate_limited'.

```bash
openprover --theorem examples/sqrt2_irrational.md \
  --headless --autonomous --max-time 30m
```

--------------------------------

### Inspect a Finished OpenProver Run

Source: https://context7.com/kripner/openprover/llms.txt

View the state and results of a completed OpenProver run in a read-only TUI. Useful for analyzing past proofs.

```bash
openprover inspect runs/sqrt2-irrational-20260217-143012
```

--------------------------------

### Managed Scratch Directory with LeanWorkDir

Source: https://context7.com/kripner/openprover/llms.txt

Creates uniquely named scratch directories within a Lean project to prevent filename collisions. Provides methods to create temporary files and write final proofs.

```python
from pathlib import Path
from openprover.lean.core import LeanWorkDir

work_dir = LeanWorkDir(project_dir=Path("./miniF2F"))
print(work_dir.dir)        # ./miniF2F/OpenProver-a3f92b1c/
print(work_dir.random_id)  # e.g. "a3f92b1c"

# Write a temp file for verification
lean_path = work_dir.make_file(
    slug="lemma_attempt",
    content="theorem foo : 1 = 1 := by rfl",
)
# ./miniF2F/OpenProver-a3f92b1c/lemma_attempt-d4e5f6.lean

# Write the final accepted proof
proof_path = work_dir.write_proof("theorem foo : 1 = 1 := by rfl")
# ./miniF2F/OpenProver-a3f92b1c/PROOF.lean
```

--------------------------------

### Parsing and Assembling Lean 4 Theorem Files with LeanTheorem

Source: https://context7.com/kripner/openprover/llms.txt

Use `LeanTheorem` to parse Lean 4 theorem files, replace `sorry` placeholders with proofs, and validate injected code. Raises `ValueError` for incorrect replacement counts or banned constructs.

```python
from openprover.lean.core import LeanTheorem

# THEOREM.lean has two sorry placeholders
raw = """.strip()

thm = LeanTheorem(raw)
print(thm.num_sorries)       # 2
print(thm.preamble_end)      # byte offset where preamble ends

# Replace each sorry with actual proof
assembled = thm.assemble_proof(
    replacements=["norm_num", "norm_num"],
    context="-- Generated by OpenProver",
)
print(assembled)
# import Mathlib
# -- Generated by OpenProver
# lemma helper : 1 + 1 = 2 := by norm_num
# theorem add : 42 + 24 = 66 := by norm_num

# Raises ValueError on wrong replacement count
try:
    thm.assemble_proof(["norm_num"])
except ValueError as e:
    print(e)  # "Expected 2 replacement(s), got 1"

# Raises ValueError on banned constructs in injected code
try:
    thm.assemble_proof(["norm_num", "sorry"])
except ValueError as e:
    print(e)  # "Replacement block 1 contains banned construct: sorry"
```

--------------------------------

### Run Lean Check in Python

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

Executes the Lean 4 compiler on a given file within a specified project directory. Returns success status and feedback.

```python
def run_lean_check(lean_file, project_dir, timeout=300):
    """Runs `lake env lean <file>` from the project directory.

    Returns `(True, "")` if returncode 0 and empty stdout; otherwise `(False, feedback)` with combined stdout/stderr.
    """
    pass
```

--------------------------------

### Run MiniF2F Benchmark with Leanstral

Source: https://context7.com/kripner/openprover/llms.txt

Execute the MiniF2F validation split benchmark using the Leanstral model. Configurable parallelism and time budgets are supported.

```python
python scripts/run_minif2f.py valid \
  --model leanstral \
  --repo-path ./miniF2F \
  --max-time 10m \
  --problem-parallelism 10
```

--------------------------------

### Claude CLI Web Search Configuration

Source: https://github.com/kripner/openprover/blob/master/DOCS.md

How to enable web search functionality in the Claude CLI by replacing the '--tools ""' argument.

```bash
claude -p --model <model> --system-prompt <...> --output-format json --permission-mode bypassPermissions --allowedTools WebSearch WebFetch
```

--------------------------------

### LLMClient - Claude CLI backend

Source: https://context7.com/kripner/openprover/llms.txt

The LLMClient interacts with Claude models via the `claude` CLI. It supports streaming, structured JSON output, web search, and tool calling.

```APIDOC
## LLMClient — Claude CLI backend

Calls Claude models via the `claude` CLI subprocess. Supports streaming, structured JSON output, web search (`WebSearch`/`WebFetch` tools), and MCP tool calling for Lean workers. Every call is archived to `archive/calls/call_NNN.json`.

```python
from pathlib import Path
from openprover.llm.claude import LLMClient

client = LLMClient(
    model="sonnet",          # "sonnet" or "opus"
    archive_dir=Path("runs/my-run/archive"),
    max_output_tokens=128_000,
    effort="high",           # "low" | "medium" | "high" | "max"
)

# Basic call — returns dict with result, cost, duration_ms, raw
response = client.call(
    prompt="Prove that sqrt(2) is irrational using contradiction.",
    system_prompt="You are a rigorous mathematician.",
)
print(response["result"])       # proof text
print(response["cost"])         # USD cost as float
print(response["duration_ms"])  # wall-clock ms

# Streaming call — stream_callback receives text chunks in real time
chunks = []
response = client.call(
    prompt="Prove that there are infinitely many primes.",
    system_prompt="You are a rigorous mathematician.",
    stream_callback=lambda text: chunks.append(text),
    label="worker-1",
)
full_text = "".join(chunks)

# Web-enabled call (requires --permission-mode bypassPermissions)
response = client.call(
    prompt="Search for Euler's proof of infinite primes and summarize.",
    system_prompt="You are a mathematical researcher.",
    web_search=True,
)

# Track cost across multiple calls
print(f"Total: {client.call_count} calls, ${client.total_cost:.4f}")

# Interrupt all active calls (e.g. from signal handler)
client.interrupt()
client.clear_interrupt()  # reset before resuming
client.cleanup()          # kill subprocesses on exit
```
```

--------------------------------

### HFClient - Local vLLM / OpenAI-compatible backend

Source: https://context7.com/kripner/openprover/llms.txt

The HFClient connects to any OpenAI-compatible HTTP server, such as vLLM. It supports streaming, reasoning extraction, and native tool calling.

```APIDOC
## HFClient — Local vLLM / OpenAI-compatible backend

Calls any OpenAI-compatible HTTP server (vLLM, serve_hf.py). Handles streaming via SSE, `<think>...</think>` reasoning extraction, and native tool calling for Lean worker tools. Cost is always 0.0 for local models.

```python
from pathlib import Path
from openprover.llm.hf import HFClient, MODEL_CONTEXT_LENGTHS

# Register a custom model context length before instantiating
MODEL_CONTEXT_LENGTHS["my-model"] = 32_768

client = HFClient(
    model="my-model",
    archive_dir=Path("runs/my-run/archive"),
    base_url="http://localhost:8000",
    answer_reserve=4096,   # tokens reserved for answer after thinking
    vllm=True,
)

# Basic inference call
response = client.call(
    prompt="Give a sketch proof that e is irrational.",
    system_prompt="You are an expert mathematician.",
    stream_callback=lambda text: print(text, end="", flush=True),
)
print(response["result"])    # answer text (after </think> boundary)
print(response["thinking"])  # chain-of-thought (inside <think>...</think>)
```
```

--------------------------------

### Budget Class

Source: https://context7.com/kripner/openprover/llms.txt

The Budget class tracks resource consumption (tokens or time) for a proving session. It supports setting limits, concluding phases, and accumulating output tokens.

```APIDOC
## Budget

Tracks the proving session's resource consumption in one of two modes: `"time"` (wall-clock seconds) or `"tokens"` (cumulative output tokens). The planner prompt receives budget status so it can pace conclusion attempts. The `conclude_after` threshold triggers a wind-down phase before full exhaustion.

```python
from openprover.budget import Budget, parse_duration

# Time-based budget: 2 hours, conclude phase at 90%
budget = Budget(mode="time", limit=parse_duration("2h"), conclude_after=0.90)

# Token-based budget: 500k output tokens
budget = Budget(mode="tokens", limit=500_000, conclude_after=0.99)

# Check state
print(budget.fraction_spent())    # 0.0 → 1.0
print(budget.is_exhausted())      # True when fraction_spent >= 1.0
print(budget.should_conclude())   # True when fraction_spent >= conclude_after
print(budget.status_str())        # "0s/2h"  or  "0/500k tok"
print(budget.summary_str())       # "0s/2h" elapsed (0%)
print(budget.limit_str())         # "2h"  or  "500k tokens"

# Accumulate tokens from LLM responses
budget.add_output_tokens(4096)
budget.add_output_tokens(8192)
print(budget.total_output_tokens)  # 12288

# Duration string parser: '30m', '2h', '1h30m', '90s', or plain seconds
assert parse_duration("1h30m") == 5400
assert parse_duration("30m")   == 1800
assert parse_duration("90s")   == 90
```
```

--------------------------------

### Verifying Lean 4 Code with run_lean_check

Source: https://context7.com/kripner/openprover/llms.txt

Compiles Lean 4 source files using `lake env lean` within a project directory. Returns a success status, feedback, and command information. Handles timeouts and memory limits.

```python
from pathlib import Path
from openprover.lean.core import run_lean_check, lean_has_errors

project_dir = Path("./miniF2F")  # must have lakefile.lean

# Write a temp Lean file to verify
lean_file = project_dir / "OpenProver-test" / "check.lean"
lean_file.parent.mkdir(exist_ok=True)
lean_file.write_text("""
import MiniF2F.ProblemImports

theorem simple : 1 + 1 = 2 := by norm_num
""")

success, feedback, cmd_info = run_lean_check(
    lean_file=lean_file,
    project_dir=project_dir,
    timeout=300,         # seconds before SIGKILL
    max_memory_mb=16384, # address-space cap (RLIMIT_AS)
)

if success:
    print("Lean check passed!")
else:
    print(f"Lean check failed:\n{feedback}")
    # cmd_info shows the exact command run
    print(cmd_info)
    # Check if it's a real error vs. just warnings
    if lean_has_errors(feedback):
        print("Contains actual errors (not just warnings)")
```

--------------------------------

### Manage Repository Items with Repo

Source: https://context7.com/kripner/openprover/llms.txt

Manages markdown and Lean files within a repository directory. Supports writing, reading, listing, resolving wikilinks, and deleting items.

```python
from pathlib import Path
from openprover.prover import Repo

repo = Repo(repo_dir=Path("runs/my-run/repo"))

# Write a new item (markdown by default)
repo.write_item(
    slug="sqrt2-proof-attempt",
    content="Summary: Contradiction approach via infinite descent.\n\nAssume sqrt(2) = p/q ...",
)
```

```python
# Write a Lean item (auto-verified if lean_project is set)
repo.write_item(
    slug="helper-lemma",
    content="-- Summary: Helper: even square implies even base\nlemma even_sq ...",
    fmt="lean",
)
```

```python
# Read a single item
content = repo.read_item("sqrt2-proof-attempt")
print(content)  # full markdown text
```

```python
# Read multiple items (formatted as sections)
text = repo.read_items(["sqrt2-proof-attempt", "helper-lemma"])
# "## [[sqrt2-proof-attempt]]\n\n...\n\n## [[helper-lemma]]\n\n..."
```

```python
# List all items (one-line index shown to planner)
index = repo.list_summaries()
# "- [[sqrt2-proof-attempt]]: Contradiction approach via infinite descent."
# "- [[helper-lemma]] (lean): Helper: even square implies even base"
```

```python
# Resolve wikilinks in a task description → returns appended reference section
task = "Use [[sqrt2-proof-attempt]] as the basis and verify formally."
refs = repo.resolve_wikilinks(task)
# "## [[sqrt2-proof-attempt]]\n\nAssume sqrt(2) = p/q ..."
```

```python
# Delete an item (pass empty content)
repo.write_item("sqrt2-proof-attempt", content=None)
```

--------------------------------

### Log Worker Tool Action in OpenProver

Source: https://context7.com/kripner/openprover/llms.txt

Logs an action performed by a worker, specifying the tool used, arguments, result, status, and duration.

```python
tui.add_worker_action(
    tab_id="worker-0",
    tool="lean_verify",
    args={"code": "theorem ..."},
    result="OK",
    status="ok",
    duration_ms=1200,
)
```

--------------------------------

### Execute Lean Worker Tool

Source: https://context7.com/kripner/openprover/llms.txt

Executes a specified Lean worker tool with given arguments. Requires LeanWorkDir and Lean project directory. Can be used for verification or storing Lean code.

```python
from openprover.lean.tools import execute_worker_tool, WORKER_TOOLS
from openprover.lean.core import LeanWorkDir
from pathlib import Path

lean_work_dir = LeanWorkDir(Path("./miniF2F"))

result_text, status = execute_worker_tool(
    name="lean_verify",
    args={"code": "theorem foo : 1 = 1 := by rfl"},
    worker_id="worker-0",
    lean_work_dir=lean_work_dir,
    lean_project_dir=Path("./miniF2F"),
    lean_explore_service=None,  # set for lean_search
)
# result_text: "OK"  or  compiler error text
# status: "ok" | "error" | "partial"
```

```python
result_text, status = execute_worker_tool(
    name="lean_store",
    args={"code": "lemma trivial : True := trivial"},
    worker_id="worker-0",
    lean_work_dir=lean_work_dir,
    lean_project_dir=Path("./miniF2F"),
    lean_explore_service=None,
)
# status "ok" → stored in _worker_stores["worker-0"] and auto-prepended
```

--------------------------------

### Budget Resource Tracking

Source: https://context7.com/kripner/openprover/llms.txt

Manages and tracks resource consumption (time or tokens) for proving sessions. Use to pace conclusion attempts and trigger wind-down phases.

```python
from openprover.budget import Budget, parse_duration

# Time-based budget: 2 hours, conclude phase at 90%
budget = Budget(mode="time", limit=parse_duration("2h"), conclude_after=0.90)

# Token-based budget: 500k output tokens
budget = Budget(mode="tokens", limit=500_000, conclude_after=0.99)

# Check state
print(budget.fraction_spent())    # 0.0 → 1.0
print(budget.is_exhausted())      # True when fraction_spent >= 1.0
print(budget.should_conclude())   # True when fraction_spent >= conclude_after
print(budget.status_str())        # "0s/2h"  or  "0/500k tok"
print(budget.summary_str())       # "0s/2h elapsed (0%)"
print(budget.limit_str())         # "2h"  or  "500k tokens"

# Accumulate tokens from LLM responses
budget.add_output_tokens(4096)
budget.add_output_tokens(8192)
print(budget.total_output_tokens)  # 12288

# Duration string parser: '30m', '2h', '1h30m', '90s', or plain seconds
assert parse_duration("1h30m") == 5400
assert parse_duration("30m")   == 1800
assert parse_duration("90s")   == 90
```

--------------------------------

### Reproduce Tool Calling Bug with Python

Source: https://github.com/kripner/openprover/blob/master/scripts/repro_leanstral_tools.md

This Python script demonstrates how to reproduce the bug by sending requests to the /v1/conversations API. It includes commented-out lines to easily switch between short and long instructions to observe the different behaviors.

```python
import json, urllib.request

payload = {
    "model": "labs-leanstral-2603",
    "inputs": [{"role": "user", "content": "Call the add tool with a=2 and b=3."}
    ],
    "instructions": "You have an add tool. Use it.",  # ← short: works
    # "instructions": "You are a helpful math assistant. Always use the add tool for arithmetic.",  # ← long: breaks
    "tools": [{
        "type": "function",
        "function": {
            "name": "add",
            "description": "Add two numbers.",
            "parameters": {
                "type": "object",
                "properties": {
                    "a": {"type": "number"},
                    "b": {"type": "number"},
                },
                "required": ["a", "b"],
            },
        },
    }],
    "stream": False,
    "completion_args": {
        "temperature": 1.0, "max_tokens": 4096, "top_p": 1, "reasoning_effort": "high",
    },
}

req = urllib.request.Request(
    "https://api.mistral.ai/v1/conversations",
    data=json.dumps(payload).encode(),
    headers={"Content-Type": "application/json", "Authorization": "Bearer <KEY>"},
)
raw = json.loads(urllib.request.urlopen(req, timeout=120).read())
print(json.dumps(raw, indent=2))
```