ArXivLean 03/2026
Math · 2026-04-21
This MathArena track evaluates tool-assisted formal theorem proving on 41 Lean 4.29.0 statements formalized from March 2026 arXiv papers. Scores report the percentage of problems whose final Lean proof passes MathArena's checker, averaged across observed problem attempts. The item count records distinct problems, not a single-run binomial denominator.
Top models (higher is better)
| Model | Score |
|---|---|
| Aristotle | 17.1 |
| GPT-5.4 | 17.1 |
| GPT-5.5 | 17.1 |
| Leanstral 1.5 119B A6B | 17.1 |
| Opus 4.7 | 14.6 |
| Gemini 3.1 Pro Preview | 14.6 |
| GLM-5.1 | 2.4 |
| Step 3.5 Flash | 0.0 |