ArXivLean 06/2026
Math
This MathArena track evaluates tool-assisted formal theorem proving on 46 Lean 4.31.0 statements formalized from June 2026 arXiv papers. Scores report the percentage of problems whose final Lean proof passes MathArena's checker, averaged across observed problem attempts. ArXivLean is refreshed every three months. The item count records distinct problems, not a single-run binomial denominator.
Top models (higher is better)
| Model | Score |
|---|---|
| GPT-6 Astra | 65.2 |
| GPT-5.6 Sol | 39.1 |
| Muse Spark 1.3 | 28.3 |
| Aristotle | 26.1 |
| Gemini 3.7 Flash | 21.7 |
| Gemini 3.8 Flash | 19.6 |
| Gemini 3.1 Pro Preview | 10.9 |
| GLM-5.2 | 8.7 |
| Step 3.7 Flash | 0.0 |