Leanstral

ID leanstral · Company Mistral AI

Leanstral [9] is a Mistral Labs model fine-tuned for Lean theorem proving using Mistral’s Vibe agent harness. The prover uses the AgentProver with the VibeHarness.

Note

The prover drives Vibe’s builtin lean agent, which pins Leanstral 1.5 (labs-leanstral-1-5). Reaching it requires Lab Model access enabled by a Mistral org admin. Vibe exposes no --model flag, so the model is fixed by the agent; the harness’s model field is recorded in the run metadata but not passed to Vibe. Vibe gates the lean agent behind an opt-in — the interactive /leanstall command — which does nothing but add "lean" to installed_agents; the harness writes that config key directly, so no interactive install step is needed.

Authentication

By default the harness reads the Mistral La Plateforme key from the host environment:

export MISTRAL_API_KEY=...

Check if the key is in your environment with:

open-atp auth-status leanstral

Alternatively, pass the key to the harness explicitly:

from open_atp.harness import VibeHarness

VibeHarness(mistral_api_key="msk-...")

Either way the harness forwards it into the sandbox as MISTRAL_API_KEY, where the lean agent’s provider reads it from the process env. See Tracking cost and usage for details.

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("leanstral", 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 leanstral

Customizing the prover

To override knobs like max_turns and max_price, construct the class directly.

from pathlib import Path

from open_atp.backends.docker import DockerBackend
from open_atp.examples import EXAMPLE, example_task
from open_atp.harness import VibeHarness
from open_atp.images import DEFAULT_IMAGE
from open_atp.provers import AgentProver

task = example_task(EXAMPLE.MUL_REORDER)
prover = AgentProver(
    harness=VibeHarness(
        max_turns=None,                  # passed to `vibe -p --max-turns`
        max_price=None,                  # passed to `vibe -p --max-price`
    ),
    backend=DockerBackend(image=DEFAULT_IMAGE),
)
result = prover.prove(task, output_dir=Path("demo"))

See the API Reference for all VibeHarness configuration options.

Harness details

By default, the Leanstral harness is equipped with:

• Official Lean skills [8].

• lean-lsp-mcp MCP server [2].

The agent prompt (below) is written into the working directory and read into $PROMPT. The Vibe CLI is then invoked in non-interactive mode with $PROMPT as the input. See the script below for the full Vibe CLI invocation.

Agent Prompt

The working directory is a complete Lean 4 lake project. One or more `.lean`
files contain `sorry` (or `admit`) placeholders standing in for proofs that have
not been written yet. Replace every such placeholder with a real proof so the
project compiles cleanly and depends on no axioms beyond Lean's standard set.

Hard rules:
- Do not weaken, rename, restate, or delete any theorem, lemma, `def`,
  `structure`, or signature. Only fill in proof bodies (the part after `:=` /
  `by` that is currently `sorry`). Changing a statement to make it easier to
  prove is failure, not success.
- No new axioms and no `sorry`/`admit`/`native_decide`-on-false escapes. The
  finished proof must type-check honestly. The only acceptable axioms are Lean's
  standard `propext`, `Classical.choice`, and `Quot.sound`.
- Stay inside this working directory; do not read or write files outside it.
- Do not edit `lakefile.toml`/`lakefile.lean`, `lean-toolchain`, or
  `lake-manifest.json` — they pin the toolchain and dependencies and must match
  the verification environment.

Workflow:
1. Find the work: search for `sorry` across the `.lean` source files (e.g.
   `rg -n '\\bsorry\\b'`). Read each file containing one to understand the
   statement, the hypotheses, and the relevant imports.
2. Confirm the lean-lsp MCP server is live before relying on it: call
   `mcp__lean-lsp__lean_diagnostic_messages` on a file you have not yet edited.
   `success:true, items:[]` means it compiles cleanly; real errors come back as
   `items`. `success:false, items:[]` usually means the import oleans aren't
   materialized yet — run `lake env lean <file>` once to build them.
3. Write a proof for one `sorry` at a time. Mathlib is available; prefer library
   lemmas, `simp`, `omega`, `linarith`, `exact?`/`apply?` suggestions, and
   `aesop` over long bespoke arguments.
4. After each edit, re-check that file with
   `mcp__lean-lsp__lean_diagnostic_messages` and iterate until it is clean.
5. When a file looks done, verify it has no stubbed proofs with
   `mcp__lean-lsp__lean_verify` — the reported axioms must NOT contain `sorryAx`.
6. Repeat until no `.lean` file contains a `sorry` and every file compiles
   cleanly. Do the final compile check per file with `lake env lean <file>`:
   exit code 0 and no output means it compiles. This is the exact command the
   grader uses, so it is the source of truth.

Tips:
- Use the lean-lsp tools (`mcp__lean-lsp__*`) as your primary feedback loop; they
  are far faster than compiling per change.
- Do NOT trust `lake build` as a compile check: the `.lean` files here are not
  lake library targets, so `lake build` reports `Build completed successfully
  (0 jobs)` without ever compiling them. Always confirm with
  `lake env lean <file>`, which compiles the file by path.
- If a goal looks false or unprovable from the given hypotheses, re-read the
  statement: you likely misread a binder or a coercion. Do not "fix" it by
  changing the statement — finish the proof as stated.
- Non-trivial proofs routinely take many rounds of compile-error fixing. Keep
  iterating against the diagnostics rather than guessing."""

src/open_atp/harness/assets/scripts/vibe_agent.sh

#!/usr/bin/env bash

# $PROMPT is exported by the AgentProver before this script runs (it reads
# agent_prompt.txt from the workdir). The backend has already cd'd into the
# workdir and symlinked .lake to the warm Mathlib cache.
#
# Mistral Vibe's `lean` agent IS Leanstral: `--agent lean` pins active_model to
# leanstral (no --model flag exists; the agent profile fixes the model). `-p`
# runs non-interactively and auto-approves all tools; the --output streaming
# event stream (newline-delimited JSON, one message per line) goes to stdout.
#
# VIBE_HOME is pinned under the workdir so vibe's config (which un-gates the
# builtin `lean` agent via installed_agents) and the per-session log -- the only
# place vibe records cost/tokens -- are sandbox-local and sync back out with the
# workdir for cost parsing.
#
# --trust trusts the workdir for this invocation (the documented flag for
# non-interactive automation). Without it vibe treats the workdir's `.vibe/` as
# an untrusted project-config folder and ignores it -- "/workspace/wd is not
# trusted; project configuration (.vibe/) will be ignored" -- silently dropping
# our config.toml (mcp_servers, bypass_tool_permissions, installed_agents).
#
# https://docs.mistral.ai/mistral-vibe/
export VIBE_HOME="$PWD/.vibe"

vibe -p "$PROMPT" \
    --agent <<AGENT>> \
    --output streaming \
    --trust \
    --workdir "$PWD"<<EXTRA>>

Tracking cost and usage

The Vibe harness provides per-session cost and token usage in its meta.json file. This is used to populate cost_usd in ProofResult. You can also monitor consumption from your Mistral La Plateforme dashboard.