Leanstral-1.5 Evaluation Results

Independent evaluation of Leanstral-1.5 — Mistral's specialized 119B MoE model for Lean 4 formal proof engineering — run locally via vLLM in July 2026.

TL;DR: Leanstral is an excellent Lean 4 proof copilot and agentic proof repair tool (grade A− overall). It is not a hands-off expert prover — always verify output with lake build.

Quick Start

Open the reports in a browser (clone the repo, then):

# macOS / Linux
open index.html          # dashboard
open LEANSTRAL_ASSESSMENT.html   # recommended starting point

Or view on GitHub Pages if enabled: set source to the repo root and open LEANSTRAL_ASSESSMENT.html.

Report	Description
LEANSTRAL_ASSESSMENT.html	Executive summary — start here
LEANSTRAL_EVAL_TIER1_RESULTS.html	Regression suite — 10 tests, per-test proofs
LEANSTRAL_EVAL_TIER2_RESULTS.html	Stress suite — 10 harder tests, per-test proofs
index.html	Navigation dashboard

Markdown versions of Tier 1 and Tier 2 are also included (.md files).

What Was Evaluated?


Model	`mistralai/Leanstral-1.5-119B-A6B`
Architecture	119B MoE (6.5B active parameters per token)
Inference	vLLM, OpenAI-compatible API on `localhost:8888`
Temperature	0.2
Tests	20 total across 2 tiers
Scoring	API response quality + extracted Lean code (not compiler-verified)

Tier 1 — Regression (10 tests)

Basic capability smoke tests: Nat induction, list properties, autoformalization, recursive function verification, number theory, and agentic proof repair.

Result: 10/10 API success · mean latency 7.2s

Tier 2 — Stress (10 tests)

Harder proofs: sorted-list insertion, BST invariant verification, finset autoformalization, Fibonacci identity, BigOperators, Ackermann positivity, and multi-error agentic repair.

Result: 10/10 API success · mean latency 32s (Fibonacci: 194s)

Key Findings

Strengths

Routine proofs (induction, lists, gcd, factorial) in 3–15 seconds with idiomatic tactics
Mathlib fluency — knows when to use Nat.dvd_trans, Finset.max', Nat.le_induction, etc.
Self-correction — caught ring failing on Nat and switched to omega mid-response
Agentic repair (best capability) — diagnoses compiler errors, fixes wrong induction variables, migrates deprecated lemmas
Hard structural proofs — 40-line BST insert proof with full case analysis
Autoformalization — correct formal types from plain-English math statements

Weaknesses

Expert algebraic proofs slow and verbose (Fibonacci: 194s, 3900 tokens)
Occasional logical gaps — some proofs may not compile without human review
Server instability on long generations (>4096 tokens can crash vLLM)
Not compiler-verified — estimated compile rate ~75–85%, not measured

Grades by Use Case

Use case	Grade
Lean 4 proof copilot	A
Agentic proof repair	A+
Autoformalization	A−
Autonomous expert prover	C+
General coding	N/A

Repository Structure

.
├── README.md                          ← you are here
├── index.html                         ← navigation dashboard
├── LEANSTRAL_ASSESSMENT.html          ← executive summary (light theme)
├── LEANSTRAL_EVAL_TIER1_RESULTS.html  ← Tier 1 detailed results
├── LEANSTRAL_EVAL_TIER2_RESULTS.html  ← Tier 2 detailed results
├── LEANSTRAL_EVAL_TIER1_RESULTS.md
├── LEANSTRAL_EVAL_TIER2_RESULTS.md
├── LEANSTRAL_EVAL_RESULTS.md          ← early Tier 1 summary (superseded)
└── results/
    ├── full_run_20260704T141512Z/     ← Tier 1 raw run
    │   ├── meta.json                  ← run metadata (model, endpoint, temp)
    │   ├── results.json               ← full API responses + latencies
    │   ├── test_*_extracted.lean      ← extracted Lean proofs per test
    │   └── test_*.md                  ← per-test model responses
    ├── tier2_run_20260704T144038Z/    ← Tier 2 raw run (same structure)
    └── smoke_test_20260704T141504Z/   ← initial single-test smoke run

Each results.json contains the full prompt, raw model response, token usage, latency, and extracted Lean blocks for every test.

Test Categories

Category	Tier 1	Tier 2	Verdict
Basic induction	✅	⚠️	Easy proofs fast; Fibonacci expert is hard
List / data structures	✅	✅	Core strength
Autoformalization	✅	✅	Correct formal types from prose
Code verification	✅	✅	BST proof is stand-out
Number theory / algebra	✅	✅	Finset sums, div/mod, monotonicity
Agentic multi-turn repair	✅	✅	Best-in-suite capability

Methodology

Each test ships compilable Lean 4 + Mathlib starter code with a sorry placeholder.
Prompts are sent to Leanstral via the OpenAI-compatible chat API.
Responses are parsed for lean code blocks and saved per test.
No lake build verification was performed — this is an API-level evaluation.

Scoring dimensions (used in assessment)

Signal	Weight
Compiles clean	40%
No `sorry` / axioms	30%
Idiomatic tactics	15%
Agentic: diagnoses prior error	10%
Conciseness	5%

Who Is Leanstral For?

Good fit:

Mathematicians formalizing proofs in Lean / Mathlib
Engineers verifying critical code (crypto, compilers, protocols)
Researchers in formal methods and theorem proving
Builders of AI agents that iterate on proofs with compiler feedback

Not a fit:

General application coding (use Claude, Codex, or a local LLM)
Guaranteed-correct proofs without human review
Work outside Lean 4 / Mathlib

Recommended workflow:

Send proof stub → Leanstral fills sorry → lake build → feed errors back → iterate

Caveats

All proofs are API-level drafts — treat every output as unverified until lake build passes.
Compile-rate estimates (~75–85%) are based on proof structure review, not measurement.
Tier 2 initially failed tests 14–20 due to a server crash; results were completed on retry.
Mathlib version was not pinned; reproducibility may vary across Mathlib releases.

License

This evaluation data and reports are provided as-is for research and reference. Leanstral and Mathlib are property of their respective owners.

Leanstral-1.5-119B-A6B_Review

Specs

README