Lean Theorem Proving Eval

---
name: lean-theorem-proving-eval
description: Evaluates a language model's ability to generate correct, step-by-step formal proof tactics for mathematical statements within the Lean 4 proof assistant. Use when the user wants to benchmark on miniF2F, or asks about evaluating this task. Reports solve_rate.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 2310.10631
  bibtex_key: [REDACTED]
  confidence: high
---

# lean-theorem-proving-eval

> Llemma: An Open Language Model For Mathematics — Azerbayev et al. (2023) (arXiv:2310.10631, 2023)

## What this evaluates

Evaluates a language model's ability to generate correct, step-by-step formal proof tactics for mathematical statements within the Lean 4 proof assistant.

## Datasets

- **miniF2F** — total 488; splits: test (488)

## Metrics

- `solve_rate` **(primary)** — range: [0, 1]
  - Fraction of formalized statements for which the model successfully generates a complete, verified proof within the specified search budget (N=1, S=32, T=100) and 10-minute timeout.

## Input / output format

**Input**: A formalized Lean 4 mathematical statement, provided alongside a 3-shot prompt containing example (tactic state, next tactic) pairs.

**Output**: A sequence of Lean 4 tactics generated iteratively via beam search, applied to the current proof state until the proof is complete or the budget/timeout is exhausted.

## Scoring recipe

```python
def compute_solve_rate(predictions, gold):
    solved = 0
    for stmt, state in zip(predictions, gold):
        tactics = beam_search_generate(stmt, N=1, S=32, T=100)
        if lean_check_proof(tactics, state, timeout=600):
            solved += 1
    return solved / len(gold)
```

## Common pitfalls

- Search budget is defined as N*S*T (3200 tactics), not just the number of attempts or iterations.
- Evaluation uses Lean 4, while some baselines (e.g., ReProver) report results on Lean 3, making direct comparison difficult.
- 10-minute timeout per statement can cause significant variance in wall-clock time across different hardware setups.

## Evidence (verbatim from paper)

> We evaluate on miniF2F (Zheng et al., 2021), which consists of 488 formalized statements from math competitions and undergraduate coursework. Given a formalized statement, the task is to generate a formal proof that is checked by Lean. We set our search budget to N = 1, S = 32, and T = 100... We generate tactics with beam search and use a 10 minute timeout.

## Citation

```bibtex
@misc{azerbayev2023llemma,
  title={Llemma: An Open Language Model For Mathematics},
  author={Azerbayev et al. (2023)},
  year={2023},
  note={arXiv:2310.10631}
}
```

- arXiv: 2310.10631