T2 Theorem Testing: leaderboard
Metric: Testing accuracy (%): share of T2's 2,206 problems from five Lean 4 repositories in which the generated theorem, substituted for the original, lets every dependent successor theorem compile; zero-shot from a natural-language statement (written by Claude Sonnet 4.5) with predecessor and successor context, one completion at temperature 0.6, top-p 0.95; higher is better. Source: arxiv.org. Saturation forecast: Around 2032. 18 models tracked.
Top models
| # | Model | Score |
|---|---|---|
| 1 | Claude Sonnet 4.5 | 38.9 |
| 2 | GPT-5 Mini | 37.9 |
| 3 | GPT-5 | 37.7 |
| 4 | Llama 3.1 70B | 37 |
| 5 | Claude 3.7 Sonnet | 36.8 |
| 6 | GPT-4o Mini | 36.7 |
| 7 | GPT-5 Nano | 36.6 |
| 8 | DeepSeek R1 | 36.3 |
| 9 | Claude Sonnet 4 | 36 |
| 10 | Llama 3.1 405B | 33.2 |
| 11 | GPT-OSS-120B | 32.3 |
| 12 | Llama 3.1 8B | 24.8 |
Interactive version: theaggregate.ai/benchmark?slug=t2-theorem-testing · How It Works · Data refreshed daily, snapshot 2026-10-07.