Gabrielebattimelli/Leanerstral-1.5-112E

Leanerstral 1.5 (112E)

Leanstral, on a diet. The same Lean 4 prover, 13% lighter, small enough to run on one GPU.

Leanerstral is Leanstral 1.5, Mistral AI's open theorem-proving model, with the 16 least-used of its 128 expert sub-networks removed from each layer and the image encoder dropped. Nothing was retrained: every remaining weight is copied byte for byte.

📄 Paper: Same Model, Fewer GPUs (Fabio Anza, UMBC; Gabriele Battimelli, Kernel Science)

At a glance

	Leanstral 1.5	Leanerstral 1.5 (112E)
experts per layer	128	112
checkpoint size	120.9 GB	105.6 GB
smallest GPU setup we ran	2x H100	1x H200
surprise on held-out Lean code (perplexity)	2.516	2.521 (+0.22%)
images	yes	no (text only)

On a single H200 it generated 1,646 tokens per second on our proof benchmark, with 32 proofs running at once.

Run it

One H200 (141 GB):

vllm serve Gabrielebattimelli/Leanerstral-1.5-112E --tensor-parallel-size 1 \
  --tokenizer-mode mistral --config-format mistral --load-format mistral \
  --tool-call-parser mistral --enable-auto-tool-choice --reasoning-parser mistral

Two H100s (80 GB): same command with --tensor-parallel-size 2.

Tested with vLLM 0.30.0 (transformers 5.16.1). Sampling as for Leanstral 1.5: temperature 1.0, reasoning effort high for hard proofs.

How fast?

Same 64 miniF2F problems, one attempt each (up to 8,192 tokens), every proof checked by Lean:

setup	model	tokens/s	tokens/s per GPU	tokens per GPU-dollar
4x H100, split 4 ways (the usual way)	Leanstral (128)	1,398	350	0.32M
2x H100, split 2 ways	Leanstral (128)	2,764	1,382	1.26M
2x H100, split 2 ways	Leanerstral (112)	2,794	1,397	1.27M
1x H200	Leanerstral (112)	1,646	1,646	1.30M

Tokens per GPU-dollar uses Modal's on-demand prices (H100 $3.95/h, H200 $4.54/h); an H200 is a bigger, faster GPU than an H100, so compare on that column.

The biggest lesson of the paper applies to the original Leanstral too: use fewer GPUs per copy. Splitting the model over 2 GPUs instead of 4 gives about 3-4x more output per GPU, with identical answers. Leanerstral goes one step further and fits on a single H200.

What did it cost in accuracy?

• On held-out Lean code: perplexity +0.22%, and 1.5 percentage points more next-token disagreement than two runs of the unmodified model already show between themselves (that noise floor is 7%).
• Proofs solved on our short benchmark: the same as the full model (too few problems to detect small differences).
• Outside Lean (chat, other languages, informal maths): not measured, probably somewhat weaker.
• No image input.

What exactly changed

1. We ran 7.7M tokens of Lean (Mathlib) through Leanstral and recorded how much each expert was used on each layer.
2. On each layer we kept the 112 busiest experts (a different set per layer). Dropped experts held 1.6% of the routing on an average layer (4.7% in the worst).
3. The router lost the matching rows, so it picks among the 112 survivors. A token whose top 4 experts all survived gets exactly the same result as before; the others get their next-best expert.
4. The image encoder (0.9 GB) was removed.

Citation

@misc{anza2026samemodel,
  title  = {Same Model, Fewer GPUs: Running a Theorem-Proving AI up to 4x More Efficiently, Without Retraining},
  author = {Anza, Fabio and Battimelli, Gabriele},
  year   = {2026},
  note   = {https://huggingface.co/Gabrielebattimelli/Leanerstral-1.5-112E}
}

License

Apache 2.0, like the base model. Leanerstral is a modification of Leanstral 1.5 by Mistral AI; the changes are listed above.