Numina

ID numina · Company Project Numina

Numina-Lean-Agent [5] is an automated theorem prover built on top of Claude Code. It adds a custom selection of skills, prompts, and search tooling to the base harness, and runs in a multi-round loop with a statement tracker. The prover uses the NuminaProver with the ClaudeCodeHarness.

Authentication

Numina runs on the Claude Code CLI, so it authenticates exactly like the Claude Code prover. Generate a long-lived OAuth token once on the host:

claude setup-token

Check you are properly authenticated with:

open-atp auth-status numina

By default NuminaProver reads CLAUDE_CODE_OAUTH_TOKEN from the host environment (for example a .env file in your project) and forwards it into the sandbox. To supply the token explicitly, pass it as the oauth_token argument to NuminaProver.

Numina’s helper skills additionally call out to Leandex / Gemini / GPT (and Claude for the informal prover). Their keys (LEAN_LEANDEX_API_KEY, GEMINI_API_KEY, OPENAI_API_KEY, and ANTHROPIC_API_KEY) are forwarded into the sandbox when present in the host env. A skill whose key is absent degrades or skips rather than failing the run. It is recommended to define all keys in a .env file in your project root.

CLAUDE_CODE_OAUTH_TOKEN=...
LEAN_LEANDEX_API_KEY=...
GEMINI_API_KEY=...
OPENAI_API_KEY=...
ANTHROPIC_API_KEY=...

Also see Tracking cost and usage.

Using the prover

Standard prover via Python API

The simplest way to run the prover is through standard_prover() which uses a standard configuration. Here, we prove the MUL_REORDER example theorem:

from pathlib import Path

from open_atp.backends.docker import DockerBackend
from open_atp.config import standard_prover
from open_atp.examples import EXAMPLE, example_task

task = example_task(EXAMPLE.MUL_REORDER)
prover = standard_prover("numina", backend=DockerBackend())
result = prover.prove(task, output_dir=Path("demo"))

Standard prover via CLI

The standard prover can also be run from the CLI:

open-atp prove path/to/task.lean output_dir numina

Customizing the prover

To override knobs like max_rounds and guard_statements, construct NuminaProver directly (the harness is fixed to Claude Code to match Numina-Lean-Agent’s configuration):

from pathlib import Path

from open_atp.backends.docker import DockerBackend
from open_atp.examples import EXAMPLE, example_task
from open_atp.images import DEFAULT_IMAGE
from open_atp.provers.numina import NuminaProver

task = example_task(EXAMPLE.MUL_REORDER)
prover = NuminaProver(
    backend=DockerBackend(image=DEFAULT_IMAGE),
    max_rounds=20,
    guard_statements=True,
)
result = prover.prove(task, output_dir=Path("demo"))

See the API Reference for all NuminaProver configuration options.

Prover details

The Numina prover uses Claude Code without any of the skills used by the other agent harnesses [8]. Instead, it defines its own set of skills and prompts. It runs a multi-round loop with a statement tracker. Each round makes a single call to the Claude Code CLI with the main_entry.md prompt below.

vendor/numina/prompts/main_entry.md

Carefully read the prompts under `.claude/prompts/subagent_prompts/` (common.md, coordinator.md, proof_agent.md, informal_agent.md, golfer.md).
Also read `.claude/skills/SKILL.md` and each sub-skill's `SKILL.md` (search, verification, llm, code-transform, sorrifier) so you know which local CLI tools are available and how to invoke them.

You should act as coordinator agent to complete the target folder / file.

When you launch a subagent, you MUST:

1. **Describe the assigned task clearly** in the prompt
2. **Include the absolute path** to its corresponding prompt file and instruct it to read and follow that prompt
3. **Include the absolute path** to the reference resources (listed below) and instruct it to read them -- they are written by expert mathematicians and are critical for the proof
4. **Instruct the subagent** to update its own target entry in CHECKLIST.md after making any progress
5. Tell the subagent to make good use of the local CLI skills in `.claude/skills/cli/` — in particular `leanexplore.py` (semantic mathlib search, invoked as `uv run --no-project .claude/skills/cli/leanexplore.py QUERY`) and `discussion_partner.py` (ask Gemini / GPT for proof strategy hints). All verification must go through `lean_check.py` (never `lake build` for per-file checks).

After a subagent returns, you MUST update CHECKLIST.md to reflect the result.

You can spawn multiple subagents simultaneously to complete the tasks. (at most 2 subagent in parallel). But MAKE SURE each subagent is working on EXACTLY ONE task.

reference resources:

Read the environment variable `REFERENCE_RESOURCES` to get the absolute path(s) of the reference material. Run:

```bash
echo "$REFERENCE_RESOURCES"
```

(or in Python: `os.environ.get("REFERENCE_RESOURCES")`). The value may be a single path or a colon-separated list of paths. If the variable is empty/unset, proceed without external references.

You should give the resolved path(s) in the prompt to the subagent.

Tracking cost and usage

The Claude Code CLI’s JSON output reports per-run cost directly. The discussion_partner skill makes API calls to Gemini and GPT — the cost of each API call is recorded in the working directory. Claude Code CLI and API costs are added to populate cost_usd in ProofResult. The helper ledger records only input and output totals, so those API calls are priced at the uncached input rate. Gemini and GPT usage can be monitored from their respective dashboards.

Warning

Unlike the Claude Code prover, the Numina prover does not solely bill your Claude plan. The discussion_partner skill makes API calls to Gemini and GPT, which can quickly become costly.